-
The Quantum Abstract Machine
Authors:
Liyi Li,
Le Chang,
Rance Cleaveland,
Mingwei Zhu,
Xiaodi Wu
Abstract:
This paper develops a model of quantum behavior that is intended to support the abstract yet accurate design and functional verification of quantum communication protocols. The work is motivated by the need for conceptual tools for the development of quantum-communication systems that are usable by non-specialists in quantum physics while also correctly capturing at a useful abstraction the underl…
▽ More
This paper develops a model of quantum behavior that is intended to support the abstract yet accurate design and functional verification of quantum communication protocols. The work is motivated by the need for conceptual tools for the development of quantum-communication systems that are usable by non-specialists in quantum physics while also correctly capturing at a useful abstraction the underlying quantum phenomena. Our approach involves defining a quantum abstract machine (QAM) whose operations correspond to well-known quantum circuits; these operations, however, are given direct abstract semantics in a style similar to that of Berry's and Boudol's Chemical Abstract Machine. This paper defines the QAM's semantics and shows via examples how it may be used to model and reason about existing quantum communication protocols.
△ Less
Submitted 20 February, 2024;
originally announced February 2024.
-
Expressiveness Results for Timed Modal Mu-Calculi
Authors:
Rance Cleaveland,
Jeroen J. A. Keiren,
Peter Fontana
Abstract:
This paper establishes relative expressiveness results for several modal mu-calculi interpreted over timed automata. These mu-calculi combine modalities for expressing passage of (real) time with a general framework for defining formulas recursively; several variants have been proposed in the literature. We show that one logic, which we call $L^{rel}_{ν,μ}$, is strictly more expressive than the ot…
▽ More
This paper establishes relative expressiveness results for several modal mu-calculi interpreted over timed automata. These mu-calculi combine modalities for expressing passage of (real) time with a general framework for defining formulas recursively; several variants have been proposed in the literature. We show that one logic, which we call $L^{rel}_{ν,μ}$, is strictly more expressive than the other mu-calculi considered. It is also more expressive than the temporal logic TCTL, while the other mu-calculi are incomparable with TCTL in the setting of general timed automata.
△ Less
Submitted 6 October, 2023;
originally announced October 2023.
-
Qafny: A Quantum-Program Verifier
Authors:
Liyi Li,
Mingwei Zhu,
Rance Cleaveland,
Alexander Nicolellis,
Yi Lee,
Le Chang,
Xiaodi Wu
Abstract:
Because of the probabilistic/nondeterministic behavior of quantum programs, it is highly advisable to verify them formally to ensure that they correctly implement their specifications. Formal verification, however, also traditionally requires significant effort. To address this challenge, we present Qafny, an automated proof system based on the program verifier Dafny and designed for verifying qua…
▽ More
Because of the probabilistic/nondeterministic behavior of quantum programs, it is highly advisable to verify them formally to ensure that they correctly implement their specifications. Formal verification, however, also traditionally requires significant effort. To address this challenge, we present Qafny, an automated proof system based on the program verifier Dafny and designed for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations modeled within a classical separation logic framework. We prove the soundness and completeness of our proof system and implement a prototype compiler that transforms Qafny programs and specifications into Dafny for automated verification purposes. We then illustrate the utility of Qafny's automated capabilities in efficiently verifying important quantum algorithms, including quantum-walk algorithms, Grover's algorithm, and Shor's algorithm.
△ Less
Submitted 19 January, 2024; v1 submitted 11 November, 2022;
originally announced November 2022.
-
Extensible Proof Systems for Infinite-State Systems
Authors:
Jeroen J. A. Keiren,
Rance Cleaveland
Abstract:
This paper revisits soundness and completeness of proof systems for proving that sets of states in infinite-state labeled transition systems satisfy formulas in the modal mu-calculus. Our results rely on novel results in lattice theory, which give constructive characterizations of both greatest and least fixpoints of monotonic functions over complete lattices. We show how these results may be used…
▽ More
This paper revisits soundness and completeness of proof systems for proving that sets of states in infinite-state labeled transition systems satisfy formulas in the modal mu-calculus. Our results rely on novel results in lattice theory, which give constructive characterizations of both greatest and least fixpoints of monotonic functions over complete lattices. We show how these results may be used to reconstruct the sound and complete tableau method for this problem due to Bradfield and Stirling. We also show how the flexibility of our lattice-theoretic basis simplifies reasoning about tableau-based proof strategies for alternative classes of systems. In particular, we extend the modal mu-calculus with timed modalities, and prove that the resulting tableaux method is sound and complete for timed transition systems.
△ Less
Submitted 26 July, 2022;
originally announced July 2022.
-
Resilience to Denial-of-Service and Integrity Attacks: A Structured Systems Approach
Authors:
Bhaskar Ramasubramanian,
M. A. Rajan,
M. Girish Chandra,
Rance Cleaveland,
Steven I. Marcus
Abstract:
The resilience of cyberphysical systems to denial-of-service (DoS) and integrity attacks is studied in this paper. The cyberphysical system is modeled as a linear structured system, and its resilience to an attack is interpreted in a graph theoretical framework. The structural resilience of the system is characterized in terms of unmatched vertices in maximum matchings of the bipartite graph and c…
▽ More
The resilience of cyberphysical systems to denial-of-service (DoS) and integrity attacks is studied in this paper. The cyberphysical system is modeled as a linear structured system, and its resilience to an attack is interpreted in a graph theoretical framework. The structural resilience of the system is characterized in terms of unmatched vertices in maximum matchings of the bipartite graph and connected components of directed graph representations of the system under attack. We first present conditions for the system to be resilient to DoS attacks when an adversary may block access or turn off certain inputs to the system. We extend this analysis to characterize resilience of the system when an adversary might additionally have the ability to affect the implementation of state-feedback control strategies. This is termed an integrity attack. We establish conditions under which a system that is structurally resilient to a DoS attack will also be resilient to a certain class of integrity attacks. Finally, we formulate an extension to the case of switched linear systems, and derive conditions for such systems to be structurally resilient to a DoS attack.
△ Less
Submitted 2 September, 2021;
originally announced September 2021.
-
Formally Verified Next-Generation Airborne Collision Avoidance Games in ACAS X
Authors:
Rachel Cleaveland,
Stefan Mitsch,
André Platzer
Abstract:
The design of aircraft collision avoidance algorithms is a subtle but important challenge that merits the need for provable safety guarantees. Obtaining such guarantees is nontrivial given the unpredictability of the interplay of the intruder aircraft decisions, the ownship pilot reactions, and the subtlety of the continuous motion dynamics of aircraft. Existing collision avoidance systems, such a…
▽ More
The design of aircraft collision avoidance algorithms is a subtle but important challenge that merits the need for provable safety guarantees. Obtaining such guarantees is nontrivial given the unpredictability of the interplay of the intruder aircraft decisions, the ownship pilot reactions, and the subtlety of the continuous motion dynamics of aircraft. Existing collision avoidance systems, such as TCAS and the Next-Generation Airborne Collision Avoidance System ACAS X, have been analyzed assuming severe restrictions on the intruder's flight maneuvers, limiting their safety guarantees in real-world scenarios where the intruder may change its course. This work takes a conceptually significant and practically relevant departure from existing ACAS X models by generalizing them to hybrid games with first-class representations of the ownship and intruder decisions coming from two independent players, enabling significantly advanced predictive power. By proving the existence of winning strategies for the resulting Adversarial ACAS X in differential game logic, collision-freedom is established for the rich encounters of ownship and intruder aircraft with independent decisions along differential equations for flight paths with evolving vertical/horizontal velocities. We present three classes of models of increasing complexity: single-advisory infinite-time models, bounded time models, and infinite time, multi-advisory models. Within each class of models, we identify symbolic conditions and prove that there then always is a possible ownship maneuver that will prevent a collision between the two aircraft.
△ Less
Submitted 1 March, 2022; v1 submitted 3 June, 2021;
originally announced June 2021.
-
Temporal-Logic Query Checking over Finite Data Streams
Authors:
Samuel Huang,
Rance Cleaveland
Abstract:
This paper describes a technique for inferring temporal-logic properties for sets of finite data streams. Such data streams arise in many domains, including server logs, program testing, and financial and marketing data; temporal-logic formulas that are satisfied by all data streams in a set can provide insight into the underlying dynamics of the system generating these streams. Our approach makes…
▽ More
This paper describes a technique for inferring temporal-logic properties for sets of finite data streams. Such data streams arise in many domains, including server logs, program testing, and financial and marketing data; temporal-logic formulas that are satisfied by all data streams in a set can provide insight into the underlying dynamics of the system generating these streams. Our approach makes use of so-called Linear Temporal Logic (LTL) queries, which are LTL formulas containing a missing subformula and interpreted over finite data streams. Solving such a query involves computing a subformula that can be inserted into the query so that the resulting grounded formula is satisfied by all data streams in the set. We describe an automaton-driven approach to solving this query-checking problem and demonstrate a working implementation via a pilot study.
△ Less
Submitted 5 June, 2020;
originally announced June 2020.
-
Timed Automata Benchmark Description
Authors:
Peter Fontana,
Rance Cleaveland
Abstract:
This report contains the descriptions of the timed automata (models) and the properties (specifications) that are used as the "benchmark examples in Data structure choices for on-the-fly model checking of real-time systems" and "The power of proofs: New algorithms for timed automata model checking." The four models from those sources are: CSMA, FISCHER, LEADER, and GRC. Additionally we include in…
▽ More
This report contains the descriptions of the timed automata (models) and the properties (specifications) that are used as the "benchmark examples in Data structure choices for on-the-fly model checking of real-time systems" and "The power of proofs: New algorithms for timed automata model checking." The four models from those sources are: CSMA, FISCHER, LEADER, and GRC. Additionally we include in this report two additional models: FDDI and PATHOS. These six models are often used to benchmark timed automata model checker speed throughout timed automata model checking papers.
△ Less
Submitted 27 May, 2020;
originally announced May 2020.
-
Better Automata through Process Algebra
Authors:
Rance Cleaveland
Abstract:
This paper shows how the use of Structural Operational Semantics (SOS) in the style popularized by the process-algebra community can lead to a more succinct and useful construction for building finite automata from regular expressions. Such constructions have been known for decades, and form the basis for the proofs of one direction of Kleene's Theorem. The purpose of the new construction is, on t…
▽ More
This paper shows how the use of Structural Operational Semantics (SOS) in the style popularized by the process-algebra community can lead to a more succinct and useful construction for building finite automata from regular expressions. Such constructions have been known for decades, and form the basis for the proofs of one direction of Kleene's Theorem. The purpose of the new construction is, on the one hand, to show students how small automata can be constructed, without the need for empty transitions, and on the other hand to show how the construction method admits closure proofs of regular languages with respect to other operators as well. These results, while not theoretically surprising, point to an additional influence of process-algebraic research: in addition to providing fundamental insights into the nature of concurrent computation, it also sheds new light on old, well-known constructions in automata theory.
△ Less
Submitted 18 February, 2020;
originally announced February 2020.
-
A Tableau Construction for Finite Linear-Time Temporal Logic
Authors:
Samuel Huang,
Rance Cleaveland
Abstract:
This paper describes a method for converting formulas in finite propositional linear-time temporal logic (Finite LTL) into finite-state automata whose languages are the models of the given formula. Finite LTL differs from traditional LTL in that formulas are interpreted with respect to finite, rather than infinite, sequences of states; this fact means that traditional finite-state automata, rather…
▽ More
This paper describes a method for converting formulas in finite propositional linear-time temporal logic (Finite LTL) into finite-state automata whose languages are the models of the given formula. Finite LTL differs from traditional LTL in that formulas are interpreted with respect to finite, rather than infinite, sequences of states; this fact means that traditional finite-state automata, rather than ω-automata such as those developed by Büchi and others, suffice for recognizing models of such formulas. The approach considered is based on well-known tableau-construction techniques developed for LTL, which we adapt here for the setting of Finite LTL. The resulting automata may be used as a basis for model checking, satisfiability testing, and model synthesis.
△ Less
Submitted 21 June, 2020; v1 submitted 16 October, 2019;
originally announced October 2019.
-
Notions of Centralized and Decentralized Opacity in Linear Systems
Authors:
Bhaskar Ramasubramanian,
Rance Cleaveland,
Steven I. Marcus
Abstract:
We formulate notions of opacity for cyberphysical systems modeled as discrete-time linear time-invariant systems. A set of secret states is $k$-ISO with respect to a set of nonsecret states if, starting from these sets at time $0$, the outputs at time $k$ are indistinguishable to an adversarial observer. Necessary and sufficient conditions to ensure that a secret specification is $k$-ISO are estab…
▽ More
We formulate notions of opacity for cyberphysical systems modeled as discrete-time linear time-invariant systems. A set of secret states is $k$-ISO with respect to a set of nonsecret states if, starting from these sets at time $0$, the outputs at time $k$ are indistinguishable to an adversarial observer. Necessary and sufficient conditions to ensure that a secret specification is $k$-ISO are established in terms of sets of reachable states. We also show how to adapt techniques for computing under-approximations and over-approximations of the set of reachable states of dynamical systems in order to soundly approximate k-ISO. Further, we provide a condition for output controllability, if $k$-ISO holds, and show that the converse holds under an additional assumption.
We extend the theory of opacity for single-adversary systems to the case of multiple adversaries and develop several notions of decentralized opacity. We study the following scenarios: i) the presence or lack of a centralized coordinator, and ii) the presence or absence of collusion among adversaries. In the case of colluding adversaries, we derive a condition for nonopacity that depends on the structure of the directed graph representing the communication between adversaries.
Finally, we relax the condition that the outputs be indistinguishable and define a notion of $ε$-opacity, and also provide an extension to the case of nonlinear systems.
△ Less
Submitted 15 March, 2019;
originally announced March 2019.
-
Bisimulation and Hennessy-Milner Logic for Generalized Synchronization Trees
Authors:
James Ferlez,
Rance Cleaveland,
Steve Marcus
Abstract:
In this work, we develop a generalization of Hennessy-Milner Logic (HML) for Generalized Synchronization Trees (GSTs) that we call Generalized Hennessy Milner Logic (GHML). Importantly, this logic suggests a strong relationship between (weak) bisimulation for GSTs and ordinary bisimulation for Synchronization Trees (STs). We demonstrate that this relationship can be used to define the GST analog f…
▽ More
In this work, we develop a generalization of Hennessy-Milner Logic (HML) for Generalized Synchronization Trees (GSTs) that we call Generalized Hennessy Milner Logic (GHML). Importantly, this logic suggests a strong relationship between (weak) bisimulation for GSTs and ordinary bisimulation for Synchronization Trees (STs). We demonstrate that this relationship can be used to define the GST analog for image-finiteness of STs. Furthermore, we demonstrate that certain maximal Hennessy-Milner classes of STs have counterparts in maximal Hennessy-Milner classes of GSTs with respect to GST weak bisimulation. We also exhibit some interesting characteristics of these maximal Hennessy-Milner classes of GSTs.
△ Less
Submitted 4 September, 2017;
originally announced September 2017.
-
An extensible formal semantics for UML activity diagrams
Authors:
Zamira Daw,
Rance Cleaveland
Abstract:
This paper presents an operational semantics for UML activity diagrams. The purpose of this semantics is three-fold: to give a robust basis for verifying model correctness; to help validate model transformations; and to provide a well-formed basis for assessing whether a proposed extension/interpretation of the modeling language is consistent with the standard. The challenges of a general formal f…
▽ More
This paper presents an operational semantics for UML activity diagrams. The purpose of this semantics is three-fold: to give a robust basis for verifying model correctness; to help validate model transformations; and to provide a well-formed basis for assessing whether a proposed extension/interpretation of the modeling language is consistent with the standard. The challenges of a general formal framework for UML models include the semi-formality of the semantics specification, the extensibility of the language, and (sometimes deliberate, sometimes accidental) under-specification of model behavior in the standard. Our approach is based on structural operational semantics, which can be extended according to domain-specific needs. The presented semantics has been implemented and tested.
△ Less
Submitted 8 April, 2016;
originally announced April 2016.
-
Corrections to A Menagerie of Timed Automata
Authors:
Jeroen J. A. Keiren,
Peter Fontana,
Rance Cleaveland
Abstract:
This note corrects a technical error in the ACM Computing Surveys paper mentioned in the title. The flaw involved constructions for showing that timed automata with urgent locations have the same expressiveness as timed automata that allow false location invariants. Corrected con- structions are presented in this note, and the affected results are reproved.
This note corrects a technical error in the ACM Computing Surveys paper mentioned in the title. The flaw involved constructions for showing that timed automata with urgent locations have the same expressiveness as timed automata that allow false location invariants. Corrected con- structions are presented in this note, and the affected results are reproved.
△ Less
Submitted 23 February, 2016;
originally announced February 2016.
-
The Power of Proofs: New Algorithms for Timed Automata Model Checking (with Appendix)
Authors:
Peter Fontana,
Rance Cleaveland
Abstract:
This paper presents the first model-checking algorithm for an expressive modal mu-calculus over timed automata, $L^{\mathit{rel}, \mathit{af}}_{ν,μ}$, and reports performance results for an implementation. This mu-calculus contains extended time-modality operators and can express all of TCTL. Our algorithmic approach uses an "on-the-fly" strategy based on proof search as a means of ensuring high p…
▽ More
This paper presents the first model-checking algorithm for an expressive modal mu-calculus over timed automata, $L^{\mathit{rel}, \mathit{af}}_{ν,μ}$, and reports performance results for an implementation. This mu-calculus contains extended time-modality operators and can express all of TCTL. Our algorithmic approach uses an "on-the-fly" strategy based on proof search as a means of ensuring high performance for both positive and negative answers to model-checking questions. In particular, a set of proof rules for solving model-checking problems are given and proved sound and complete; we encode our algorithm in these proof rules and model-check a property by constructing a proof (or showing none exists) using these rules. One noteworthy aspect of our technique is that we show that verification performance can be improved with \emph{derived rules}, whose correctness can be inferred from the more primitive rules on which they are based. In this paper, we give the basic proof rules underlying our method, describe derived proof rules to improve performance, and compare our implementation of this model checker to the UPPAAL tool.
△ Less
Submitted 28 August, 2014; v1 submitted 26 August, 2014;
originally announced August 2014.
