An Adequate Semantics for Hybrid While
Hybrid computation combines discrete and continuous dynamics in the form of an entangled mixture inherently present both in natural phenomena, and in applications ranging from control theory to microbiology. The emergent behaviours bear signs of both computational and physical processes, and thus present difficulties not only for analysis, but also for describing them adequately in a structural, well-founded way. We present a while-language for deterministic hybrid computation HybCore and equip it with an operational and computationally adequate denotational semantics over a hybrid monad. As an intermediate step we develop a more lightweight duration semantics drawing on a duration monad that we introduce as a lightweight counterpart to the hybrid monad.
Sun 7 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 18:00 | |||
16:00 30mTalk | Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs QAPL Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski RWTH Aachen University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja RWTH Aachen University, Thomas Noll RWTH Aachen University DOI | ||
16:30 30mTalk | An Adequate Semantics for Hybrid While QAPL | ||
17:00 30mTalk | Recent Applications and Quantitative Aspects of Spatial Model Checking QAPL | ||
17:30 30mTalk | Equational Characterization Metaresults for Bisimulation and Trace Semantics in ULTraS QAPL Marco Bernardo University of Urbino |