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.
We investigate decision procedures for quantifier-free fragments of set theory extended with relational and cardinality constraints. While the satisfiability problem for the general fragment is undecidable due to the existence of reductions from Hilbert’s 10th problem, in this article we show that extensions of existential Presburger arithmetic with atoms of the form \(x\leq y^{d}\) or of the form \(y^{d}\leq x\) , where \(d\in\mathbb{N}\) , are decidable in non-deterministic polynomial time. We apply these results to fragments of quantifier-free relational logic. Our methods rely on a normal form for linear constraints, which may be of independent interest.
Most modern (classical) programming languages support recursion. Recursion has also been successfully applied to the design of several quantum algorithms and introduced in a couple of quantum programming languages. So, it can be expected that recursion will become one of the fundamental paradigms of quantum programming. In addition, ancilla quantum data, e.g., ancilla qubits, have been extensively employed in designing various quantum algorithms, especially in the design of quantum circuits, and are also included in the mainstream quantum programming languages. Several program logics have been developed for the verification of quantum While-programs. However, there are as yet no general methods for reasoning about general recursive procedures with parameter passing and ancilla data in quantum computing (with measurement). We fill the gap in this article by proposing a parameterized quantum assertion logic and, based on which, designing a Hoare logic for verifying parameterized recursive quantum programs with ancilla data and probabilistic control (induced by quantum measurement). The assertion logic is a unifying framework for defining various assertions of both classical (deterministic or probabilistic) and quantum programs. Besides proving partial and total correctness of the above quantum programs, the Hoare logic can be used to prove probabilistic correctness of these programs by reducing it to total correctness. Concretely, an axiomatic basis of reasoning with both approximate and exact probabilities is established grounded on the soundness and completeness theorem of the Hoare logic. In particular, two counterexamples for illustrating incompleteness of non-parameterized assertions in verifying recursive procedures, and, one counterexample for showing the failure of reasoning with exact probabilities based on partial correctness, are constructed. The effectiveness of our logic in verifying quantum programs with the above mechanisms is shown by three main examples—recursive quantum Markov chain (with probabilistic control), fixed-point Grover’s search, and recursive quantum Fourier sampling. What’s more, the successful verification of recursive quantum Fourier sampling illustrates that the Hoare logic has the potential in verifying more complicated programs, e.g., with data structure of arrays and functionality of quantum uncomputation (i.e., restoring the allocated quantum data to their original state before deallocation).
The set of binary decision diagrams , an efficient data structure representing Boolean functions, is extensively used in many distinct contexts like model verification, machine learning, cryptography or also resolution of combinatorial problems. The most famous variant, called reduced ordered binary decision diagram ( robdd for short), can be viewed as the result of a specific compaction of a complete decision tree. A great property is that, once an order over the Boolean variables is fixed, each Boolean function is represented by exactly one robdd . In this paper we aim at computing the exact distribution of the Boolean functions in \(k\) variables according to the robdd size . Recall the number of Boolean functions with \(k\) variables is equal to \(2^{2^{k}}\) , which is of double exponential growth with respect to the number of variables. The maximal size of an robdd with \(k\) variables is \(M_{k}\approx 2^{k}/k\) . In this paper, we develop the first polynomial algorithm to derive the distribution of Boolean functions over \(k\) variables with respect to robdd size denoted by \(n\) . It performs \(O(k\;n^{3}\log n)\) arithmetic operations on integers and necessitates to store \(O(n^{2})\) integers in memory storage; note that the maximal size of integers involved in the computations is \(O(k\;2^{k})\) bits. Our new approach relies on a decomposition of robdd s layer by layer and on an enumerative inclusion-exclusion argument.
Twin-width is a powerful graph invariant that supports the efficient solution of various NP-hard problems when the input graph has a bounded twin-width. First-order model checking is fixed-parameter tractable on graph classes of bounded twin-width. This work introduces two algorithmic strategies for exact twin-width computation: SAT encodings and a Branch & Bound approach. The SAT encodings explore distinct formulations of twin-width, enhancing performance across different instance types; the Branch & Bound algorithm leverages cached partial solutions for improved efficiency on larger graphs. We propose a verification framework combining these methods and yield verifiable proofs for computed twin-width. Our research contributes conceptual insights into twin-width computation, including new contraction orderings and lower and upper bound techniques that can be of independent interest. We accompany our theoretical developments with a rigorous experimental evaluation.
Equational problems are fundamental in computer science, frequently arising as subproblems across diverse domains, including program analysis and learning from examples and counterexamples. This article focuses on equational problems in languages with binding operators, formulating them within the nominal framework and referring to them as Nominal Equational Problems. We provide a comprehensive definition of solutions for nominal equational problems and introduce a set of simplification rules for computing these solutions within the nominal ground term algebra. We rigorously prove that the simplification rules are sound, solution-preserving and complete. Moreover, we establish that, under a specific strategy for rule application, the simplification process always terminates, thereby providing an effective algorithm for solving nominal equational problems. Finally, we demonstrate the practical relevance of our results by showcasing how nominal equational problems can serve as a framework for learning from examples and counterexamples. We also illustrate their applicability in addressing sufficient completeness problems, emphasising their utility in theoretical and practical contexts.
Constant-rate multi-mode systems (MMSs) are hybrid systems with finitely many modes and real-valued variables that evolve over continuous time according to mode-specific constant rates. Equivalently, they correspond to continuous vector addition systems (VASs), where counters may become negative. We introduce a variant of linear temporal logic (LTL) for MMS, and we investigate the complexity of the model-checking problem for syntactic fragments of LTL. We obtain a complexity trichotomy: Each fragment is either P-complete, NP-complete, or undecidable. Since our logic can constrain the counters to remain non-negative, it further applies to continuous VAS. Thus, our results yield a framework for MMS and continuous VAS that generalizes and unify several existing results.
Higher-order logic HOL offers a very simple syntax and semantics for knowledge representation and reasoning in various particular domains, including in particular representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms. Dependent type theory offers such a rich type system, but has rather substantial conceptual differences to HOL, as well as comparatively poor proof automation support. We introduce a dependently-typed extension DHOL of HOL that retains the style and conceptual framework of HOL. Moreover, we build a translation from DHOL to HOL and implement it as a preprocessor to HOL theorem provers able to parse TPTP, thereby making all such provers able to run on DHOL problems.
Larrauri and Živný [ICALP'25/ACM ToCL'24] recently established a complete complexity classification of the problem of solving a system of equations over a monoid N assuming that a solution exists over a monoid M, where both monoids are finite and M admits a homomorphism to N. Using the algebraic approach to promise constraint satisfaction problems, we extend their complexity classification in two directions: we obtain a complexity dichotomy in the case where arbitrary relations are added to the monoids, and we moreover allow the monoid M to be finitely generated.
We study descriptive complexity of counting complexity classes in the range from #P to # NP. The proof of Fagin's characterization of NP by existential second-order logic generalizes to the counting setting in the following sense: The class #P can be logically described as the class of functions counting satisfying assignments to free relation variables in first-order formulae. This was first observed by Saluja et al. In this article, we extend this study to classes beyond #P and extensions of first-order logic with team semantics. These team-based logics are closely related to existential second-order logic and its fragments, hence our results also shed light on the complexity of counting for extensions of first-order logic in Tarski's semantics. Our results show that the class # NP can be logically characterized by independence logic and existential second-order logic, whereas dependence logic and inclusion logic give rise to subclasses of # NP and #P, respectively. We further relate the class obtained from inclusion logic to the complexity class TotP subset of #P.
We study the problem of counting answers to unions of conjunctive queries (UCQs) under structural restrictions on the input query. Concretely, given a class C of UCQs, the problem #UCQ(C) provides as input a UCQ Q in C and a database D and the problem is to compute the number of answers of Q in D. Chen and Mengel [PODS'16] have shown that for any recursively enumerable class C, the problem #UCQ(C) is either fixed-parameter tractable or hard for one of the parameterised complexity classes W[1] or #W[1]. However, their tractability criterion is unwieldy in the sense that, given any concrete class C of UCQs, it is not easy to determine how hard it is to count answers to queries in C. Moreover, given a single specific UCQ Q, it is not easy to determine how hard it is to count answers to Q. In this work, we address the question of finding a natural tractability criterion: The combined conjunctive query of a UCQ $\varphi_1 \vee \dots \vee \varphi_\ell$ is the conjunctive query $\varphi_1 \wedge \dots \wedge \varphi_\ell$. We show that under natural closure properties of C, the problem #UCQ(C) is fixed-parameter tractable if and only if the combined conjunctive queries of UCQs in C, and their contracts, have bounded treewidth. A contract of a conjunctive query is an augmented structure, taking into account how the quantified variables are connected to the free variables. If all variables are free, then a conjunctive query is equal to its contract; in this special case the criterion for fixed-parameter tractability of #UCQ(C) thus simplifies to the combined queries having bounded treewidth. Finally, we give evidence that a closure property on C is necessary for obtaining a natural tractability criterion: We show that even for a single UCQ Q, the meta problem of deciding whether #UCQ({Q}) can be solved in time $O(|D|^d)$ is NP-hard for any fixed $d\geq 1$.
We present results concerning the expressiveness and decidability of a popular graph learning formalism, graph neural networks (GNNs), exploiting connections with logic. We use a family of recently-discovered decidable logics involving "Presburger quantifiers". We show how to use these logics to measure the expressiveness of classes of GNNs, in some cases getting exact correspondences between the expressiveness of logics and GNNs. We also employ the logics, and the techniques used to analyze them, to obtain decision procedures for verification problems over GNNs. We complement this with undecidability results for static analysis problems involving the logics, as well as for GNN verification problems.
Valued constraint satisfaction problems (VCSPs) constitute a large class of computational optimisation problems. It was shown recently that, over finite domains, every VCSP is in P or NP-complete, depending on the admitted cost functions. In this article, we study cost functions over countably infinite domains whose automorphisms form an oligomorphic permutation group. Our results include a hardness condition based on a generalisation of pp-constructability as known from classical CSPs and a polynomial-time tractability condition based on the concept of fractional polymorphisms. We then observe that the resilience problem for unions of conjunctive queries (UCQs) studied in database theory, under bag semantics, may be viewed as a special case of the VCSPs that we consider. We obtain a complexity dichotomy for the case of incidence-acyclic UCQs and exemplarily use our methods to determine the complexity of a query that had remained open in the literature. Further, we conjecture that our hardness and tractability conditions match for resilience problems for UCQs.
This paper focuses on the runtime verification of hyperproperties expressed in HypermuHML, an expressive yet simple logic for describing properties of sets of traces. To this end, we first consider a simple language of monitors that can observe sets of system executions and report verdicts w.r.t. a given HypermuHML formula. In this setting, a unique omniscient monitor observes all system traces, and, in this sense, it is 'centralized'. However, in a possibly distributed system, having a centralized entity is undesirable; hence, we also provide a language for 'decentralized' monitors, where each trace has its own monitor, and monitors for different traces can yield a unique verdict by communicating their observations. For both the centralized and the decentralized settings, we provide a synthesis procedure that, given a formula, yields a monitor that is correct (i.e., sound and violation complete). A key step in proving the correctness of the synthesis for decentralized monitors is a result showing that, for each formula, the synthesized centralized monitor and its corresponding decentralized one are weakly bisimilar for a suitable notion of weak bisimulation.
Arranging the bits of a random string or real into k columns of a two-dimensional array or higher dimensional structure is typically accompanied with loss in the Kolmogorov complexity of the columns, which depends on k. We quantify and characterize this phenomenon for arrays and trees and its relationship to negligible classes.
We address the problem of model checking context-free specifications for probabilistic pushdown automata, which has relevant applications in the verification of recursive probabilistic programs. Operator Precedence Languages (OPLs) are an expressive subclass of context-free languages suitable for model checking recursive programs. The derived Precedence Oriented Temporal Logic (POTL) can express fundamental OPL specifications such as pre/post-conditions and exception safety. We introduce probabilistic Operator Precedence Automata (pOPA), a class of probabilistic pushdown automata whose traces are OPLs, and study their model checking problem against POTL specifications. We identify a fragment of POTL, called POTLfχ, for which we develop an EXPTIME algorithm for qualitative probabilistic model checking, and an EXPSPACE algorithm for the quantitative variant. The algorithms rely on the property of separation of automata generated from POTLfχ formulas. The same property allows us to employ these algorithms for model checking pOPA against Linear Temporal Logic (LTL) specifications. POTLfχ is then the first context-free logic for which an optimal probabilistic model checking algorithm has been developed, matching its EXPTIME lower bound in complexity. In comparison, the best known algorithm for probabilistic model checking of CaRet, a prominent temporal logic based on Visibly Pushdown Languages (VPL), is doubly exponential.
