Dynamic logic is a powerful approach to reasoning about programs and their executions, obtained by extending classical logic with modalities that can express program executions as formulas. However, the use of dynamic logic in the setting of concurrency has proved problematic because of the challenge of capturing interleaving. This challenge stems from the fact that, traditionally, programs are represented by their sets of traces. These sets are then expressed as elements of a Kleene algebra, for which it is not possible to decide equality in the presence of the commutations required to model interleaving. In this work, we generalise propositional dynamic logic (PDL) to a logic framework we call operational propositional dynamic logic (OPDL), which departs from tradition by distinguishing programs from their traces. Traces are generated by an arbitrary operational semantics that we take as a parameter, making our approach applicable to different program syntaxes and semantics. To develop our framework, we provide the first proof of cut-elimination for a finitely-branching non-wellfounded sequent calculus for PDL. Thanks to this result we can effortlessly prove adequacy for PDL, and extend these results to OPDL. We conclude by discussing OPDL for two representative cases of concurrency: the Calculus of Communicating Systems (CCS), where interleaving is obtained by parallel composition, and Choreographic Programming, where interleaving is obtained by out-of-order execution.
There exists extensive research on formal verification methods for timed discrete event systems. These formalisms are usually considered in the dense (or continuous) time model. Dense time semantics allow accurate modeling of real-world systems, but often lead to undecidability results for many verification problems, even if heavily restricted subclasses are considered. To overcome these limitations, timed behavior is often approximated using the discrete time model where time progresses only in discrete steps. However, these works almost exclusively consider single classes like timed automata or time Petri nets and rarely study how these classes relate. While the relationships between timed discrete event systems are well understood in the dense time model, there exist almost no results for the discrete time model. In this paper, we aim to close this gap. We develop a language-theoretic classification of several classes of discrete-time discrete event systems (DTDES). We consider timed automata, time Petri nets, constant-time automata, and tick automata, all with discrete time semantics. We study each class with multiple semantic extensions like silent transitions, periodic time constraints, and arbitrary clock updates. We classify these formalisms by their expressiveness, provide, where possible, transformations between different classes of DTDES, and analyze their worst-case complexity. Our classification unifies DTDES in terms of expressiveness and thus provides insights into generalizing verification methods from one class to others by means of reduction.
Multiparty session types (MPST) serve as a foundational framework for formally specifying and verifying message-passing protocols. Asynchronous subtyping in MPST allows for typing optimised programs preserving type safety and deadlock freedom under asynchronous interactions where the order of messages sent (resp. received) to (resp. from) particular participant is preserved and sending is non-blocking. The optimisation is achieved by reordering send actions with any other action, except sends to the same participant, and by reordering receive actions with other receive actions, except those from the same participant. Sound subtyping algorithms have been extensively studied and implemented as part of various programming languages and tools including C, Rust and C-MPI. However, formalising all such permutations under sequencing, selection, branching and recursion in session types is an intricate task. Additionally, checking asynchronous subtyping has been proven to be undecidable. This article presents the first formalisation of asynchronous subtyping for MPST within the Coq proof assistant. We begin by translating session types into session trees , unfolding recursion coinductively. These trees are then decomposed into new tree forms that incorporate singleton branching and/or selection constructs. On these trees, which involve both singleton branching and selections, we define action reorderings within a coinductive refinement relation that governs subtyping. To demonstrate the expressiveness of our formalisation, we verify several subtyping schemas drawn from the literature—none of which can be simultaneously validated by existing decidable but sound algorithms. Additionally, we take the (inductive) negation of the refinement relation from a prior work by Ghilezan et al. and re-implement it, significantly reducing the number of rules (from eighteen to eight). We establish the completeness of subtyping with respect to its negation in Coq. We establish the correctness of the refinement relation, in Coq, showing that it preserves the ordering of send (resp. receive) actions to (resp. from) a specific participant. Additionally, we formally demonstrate in Coq that refinement is transitive, a property crucial for closing certain cases in subtyping proofs. In the formalisation, we use the greatest fixed point of the least fixed point technique, facilitated by the Paco library, to define coinductive predicates. We employ parametrised coinduction to prove their properties. The formalisation consists of roughly 32K lines of Coq code and is available on GitHub at https://github.com/ekiciburak/async-mpst-st/tree/acm and on Zenodo at https://doi.org/10.5281/zenodo.18268293 .
There is extensive literature on automated test generation using reactive design models, where control is determined by events. In contrast, the (idealised) simulation paradigm defines control through cycles dictated by the passage of time. Within each cycle, inputs are read and processed, and outputs are provided, all instantaneously, and afterwards time progresses. To exercise a simulation using tests generated from a reactive design model requires changes to the tests to take into account this paradigm shift. This article focuses on automation of the necessary changes and of the use of the resulting tests in a simulation campaign. Based on a notion of conformance that establishes whether a simulation is correct with respect to a reactive design, we (1) identify the reactive tests that are meaningful; (2) define a process to convert those tests; (3) provide an algorithm to execute those tests and (4) prove soundness and completeness of our approach. Our work is described in the context of the RoboStar framework for model-based development of control software for robotics applications, and its process algebraic semantics. The testing approach we propose here represents a significant advancement in the current testing practices within the field of robotics, where simulations are widely used.
Hyperproperties are a modern specification paradigm that extends properties of a single trace to express properties of a set of traces. Temporal logics for hyperproperties studied in the literature, including HyperLTL, assume a synchronous semantics and enjoy a decidable model checking problem. In this article, we introduce two asynchronous and orthogonal extensions of HyperLTL, Stuttering HyperLTL (HyperLTL \({}_{S}\) ) and Context HyperLTL (HyperLTL \({}_{C}\) ). Both of these extensions are useful, for instance, to formulate asynchronous variants of information-flow security properties. We show that for these logics, model checking is in general undecidable. On the positive side, for each of them, we identify a fragment with a decidable model checking problem that subsumes HyperLTL and that can express meaningful asynchronous requirements. Moreover, we provide the exact computational complexity of model checking for these two fragments which, for the HyperLTL \({}_{S}\) fragment, coincides with that of the strictly less expressive logic HyperLTL.
