Related papers: Dynamic Logic of Communicating Hybrid Programs
This article presents a relatively complete proof calculus for the dynamic logic of communicating hybrid programs dLCHP. Beyond hybrid systems, communicating hybrid programs not only feature mixed discrete and continuous dynamics but also…
This paper introduces a uniform substitution calculus for $\mathsf{dL}_\text{CHP}$, the dynamic logic of communicating hybrid programs. Uniform substitution enables parsimonious prover kernels by using axioms instead of axiom schemata.…
Computer-Controlled Systems (CCS) are a subclass of hybrid systems where the periodic relation of control components to time is paramount. Since they additionally are at the heart of many safety-critical devices, it is of primary importance…
Deductive verification of hybrid systems (HSs) increasingly attracts more attention in recent years because of its power and scalability, where a powerful specification logic for HSs is the cornerstone. Often, HSs are naturally modelled by…
Deductive methods for the verification of hybrid systems vary on the format of statements in correctness proofs. Building on the example of Hoare triple-based reasoning, we have investigated several such methods for systems described in…
Signal temporal logic (STL) was introduced for monitoring temporal properties of continuous-time signals for continuous and hybrid systems. Differential dynamic logic (dL) was introduced to reason about the end states of a hybrid program.…
Formally specifying, let alone verifying, properties of systems involving multiple programming languages is inherently challenging. We introduce Heterogeneous Dynamic Logic (HDL), a framework for combining reasoning principles from distinct…
We combine quantified differential dynamic logic (QdL) for reasoning about the possible behavior of distributed hybrid systems with temporal logic for reasoning about the temporal behavior during their operation. Our logic supports…
Differential dynamic logic (dL) is a formal framework for specifying and reasoning about hybrid systems, i.e., dynamical systems that exhibit both continuous and discrete behaviors. These kinds of systems arise in many safety- and…
Real world systems of interest often feature interactions between discrete and continuous dynamics. Various hybrid system formalisms have been used to model and analyze this combination of dynamics, ranging from mathematical descriptions,…
We address a fundamental mismatch between the combinations of dynamics that occur in cyber-physical systems and the limited kinds of dynamics supported in analysis. Modern applications combine communication, computation, and control. They…
Probabilistic and stochastic behavior are omnipresent in computer controlled systems, in particular, so-called safety-critical hybrid systems, because of fundamental properties of nature, uncertain environments, or simplifications to…
We survey dynamic logics for specifying and verifying properties of dynamical systems, including hybrid systems, distributed hybrid systems, and stochastic hybrid systems. A dynamic logic is a first-order modal logic with a pair of…
We present a tool called HHLPar for verifying hybrid systems modelled in Hybrid Communicating Sequential Processes (HCSP). HHLPar is built upon a Hybrid Hoare Logic for HCSP, which is able to reason about continuous-time properties of…
Ensuring that safety-critical applications behave as intended is an important yet challenging task. Modeling languages like differential dynamic logic (dL) have proof calculi capable of proving guarantees for such applications. However, dL…
Switched systems are known to exhibit subtle (in)stability behaviors requiring system designers to carefully analyze the stability of closed-loop systems that arise from their proposed switching control laws. This paper presents a formal…
We present a theory of parameterized dynamic logic, namely DLp, for specifying and reasoning about a rich set of program models based on their transitional behaviours. Different from most dynamic logics that deal with regular expressions or…
Applying dynamic logics to program verifications is a challenge, because their axiomatic rules for regular expressions can be difficult to be adapted to different program models. We present a novel dynamic logic, called DLp, which supports…
This work presents three increasingly expressive Dynamic Logics in which the programs are CCS processes (sCCS-PDL, CCS-PDL and XCCS-PDL). Their goal is to reason about properties of concurrent programs and systems described using CCS. In…
In this article, the decidability and computability issues of dynamic probability logic (DPL) are addressed. Firstly, a proof system $\mathcal{H}_{DPL}$ is introduced for DPL and shown that it is weakly complete. Furthermore, this logic has…