Showing 1–50 of 52 results for author: Platzer, A

Intersymbolic AI: Interlinking Symbolic AI and Subsymbolic AI

Authors: André Platzer

Abstract: This perspective piece calls for the study of the new field of Intersymbolic AI, by which we mean the combination of symbolic AI, whose building blocks have inherent significance/meaning, with subsymbolic AI, whose entirety creates significance/effect despite the fact that individual building blocks escape meaning. Canonical kinds of symbolic AI are logic, games and planning. Canonical kinds of su… ▽ More This perspective piece calls for the study of the new field of Intersymbolic AI, by which we mean the combination of symbolic AI, whose building blocks have inherent significance/meaning, with subsymbolic AI, whose entirety creates significance/effect despite the fact that individual building blocks escape meaning. Canonical kinds of symbolic AI are logic, games and planning. Canonical kinds of subsymbolic AI are (un)supervised machine and reinforcement learning. Intersymbolic AI interlinks the worlds of symbolic AI with its compositional symbolic significance and meaning and of subsymbolic AI with its summative significance or effect to enable culminations of insights from both worlds by going between and across symbolic AI insights with subsymbolic AI techniques that are being helped by symbolic AI principles. For example, Intersymbolic AI may start with symbolic AI to understand a dynamic system, continue with subsymbolic AI to learn its control, and end with symbolic AI to safely use the outcome of the learned subsymbolic AI controller in the dynamic system. Intersymbolic AI combines both symbolic and subsymbolic AI to increase the effectiveness of AI compared to either kind of AI alone, in much the same way that the combination of both conscious and subconscious thought increases the effectiveness of human thought compared to either kind of thought alone. Some successful contributions to the Intersymbolic AI paradigm are surveyed here but many more are considered possible by advancing Intersymbolic AI. △ Less

Submitted 17 June, 2024; originally announced June 2024.

MSC Class: 68T01; 68T05; 68T07; 68T27; 68T30; 03B70 ACM Class: I.2.0; I.2.3; I.2.4; I.2.6; I.2.8

Uniform Substitution for Differential Refinement Logic

Authors: Enguerrand Prebet, André Platzer

Abstract: This paper introduces a uniform substitution calculus for differential refinement logic dRL. The logic dRL extends the differential dynamic logic dL such that one can simultaneously reason about properties of and relations between hybrid systems. Refinements are useful e.g. for simplifying proofs by relating a concrete hybrid system to an abstract one from which the property can be proved more eas… ▽ More This paper introduces a uniform substitution calculus for differential refinement logic dRL. The logic dRL extends the differential dynamic logic dL such that one can simultaneously reason about properties of and relations between hybrid systems. Refinements are useful e.g. for simplifying proofs by relating a concrete hybrid system to an abstract one from which the property can be proved more easily. Uniform substitution is the key to parsimonious prover microkernels. It enables the verbatim use of single axiom formulas instead of axiom schemata with soundness-critical side conditions scattered across the proof calculus. The uniform substitution rule can then be used to instantiate all axioms soundly. Access to differential variables in dRL enables more control over the notion of refinement, which is shown to be decidable on a fragment of hybrid programs. △ Less

Submitted 31 May, 2024; v1 submitted 25 April, 2024; originally announced April 2024.

Comments: IJCAR 2024

ACM Class: F.3.1; F.4.1; D.2.4

Complete Game Logic with Sabotage

Authors: Noah Abou El Wafa, André Platzer

Abstract: Game Logic with sabotage ($\mathsf{GL_s}$) is introduced as a simple and natural extension of Parikh's game logic with a single additional primitive, which allows players to lay traps for the opponent. $\mathsf{GL_s}$ can be used to model infinite sabotage games, in which players can change the rules during game play. In contrast to game logic, which is strictly less expressive, $\mathsf{GL_s}$ is… ▽ More Game Logic with sabotage ($\mathsf{GL_s}$) is introduced as a simple and natural extension of Parikh's game logic with a single additional primitive, which allows players to lay traps for the opponent. $\mathsf{GL_s}$ can be used to model infinite sabotage games, in which players can change the rules during game play. In contrast to game logic, which is strictly less expressive, $\mathsf{GL_s}$ is exactly as expressive as the modal $μ$-calculus. This reveals a close connection between the entangled nested recursion inherent in modal fixpoint logics and adversarial dynamic rule changes characteristic for sabotage games. A natural Hilbert-style proof calculus for $\mathsf{GL_s}$ is presented and proved complete using syntactic equiexpressiveness reductions. The completeness of a simple extension of Parikh's calculus for game logic follows. △ Less

Submitted 4 June, 2024; v1 submitted 15 April, 2024; originally announced April 2024.

Comments: To appear at LICS 2024

MSC Class: 03B70 (Primary) 03B45; 68Q60; 91A44; 91A05; 91A25 (Secondary) ACM Class: F.3.1; F.4.1; F.3.3

Provably Safe Neural Network Controllers via Differential Dynamic Logic

Authors: Samuel Teuber, Stefan Mitsch, André Platzer

Abstract: While neural networks (NNs) have potential as autonomous controllers for Cyber-Physical Systems, verifying the safety of NN based control systems (NNCSs) poses significant challenges for the practical use of NNs, especially when safety is needed for unbounded time horizons. One reason is the intractability of analyzing NNs, ODEs and hybrid systems. To this end, we introduce VerSAILLE (Verifiably S… ▽ More While neural networks (NNs) have potential as autonomous controllers for Cyber-Physical Systems, verifying the safety of NN based control systems (NNCSs) poses significant challenges for the practical use of NNs, especially when safety is needed for unbounded time horizons. One reason is the intractability of analyzing NNs, ODEs and hybrid systems. To this end, we introduce VerSAILLE (Verifiably Safe AI via Logically Linked Envelopes): The first general approach that allows reusing control theory results for NNCS verification. By joining forces, we exploit the efficiency of NN verification tools while retaining the rigor of differential dynamic logic (dL). Based on provably safe control envelopes in dL, we derive specifications for the NN which is proven via NN verification. We show that a proof of the NN adhering to the specification is mirrored by a dL proof on the infinite-time safety of the NNCS. The NN verification properties resulting from hybrid systems typically contain nonlinear arithmetic and arbitrary logical structures while efficient NN verification merely supports linear constraints. To overcome this divide, we present Mosaic: An efficient, sound and complete verification approach for polynomial real arithmetic properties on piece-wise linear NNs. Mosaic partitions complex verification queries into simple queries and lifts off-the-shelf linear constraint tools to the nonlinear setting in a completeness-preserving manner by combining approximation with exact reasoning for counterexample regions. Our evaluation demonstrates the versatility of VerSAILLE and Mosaic: We prove infinite-time safety on the classical Vertical Airborne Collision Avoidance NNCS verification benchmark for two scenarios while (exhaustively) enumerating counterexample regions in unsafe scenarios. We also show that our approach significantly outperforms State-of-the-Art tools in closed-loop NNV. △ Less

Submitted 14 June, 2024; v1 submitted 16 February, 2024; originally announced February 2024.

Comments: 35 pages (main paper has 9 pages), 12 figures

CESAR: Control Envelope Synthesis via Angelic Refinements

Authors: Aditi Kabra, Jonathan Laurent, Stefan Mitsch, André Platzer

Abstract: This paper presents an approach for synthesizing provably correct control envelopes for hybrid systems. Control envelopes characterize families of safe controllers and are used to monitor untrusted controllers at runtime. Our algorithm fills in the blanks of a hybrid system's sketch specifying the desired shape of the control envelope, the possible control actions, and the system's differential eq… ▽ More This paper presents an approach for synthesizing provably correct control envelopes for hybrid systems. Control envelopes characterize families of safe controllers and are used to monitor untrusted controllers at runtime. Our algorithm fills in the blanks of a hybrid system's sketch specifying the desired shape of the control envelope, the possible control actions, and the system's differential equations. In order to maximize the flexibility of the control envelope, the synthesized conditions saying which control action can be chosen when should be as permissive as possible while establishing a desired safety condition from the available assumptions, which are augmented if needed. An implicit, optimal solution to this synthesis problem is characterized using hybrid systems game theory, from which explicit solutions can be derived via symbolic execution and sound, systematic game refinements. Optimality can be recovered in the face of approximation via a dual game characterization. The resulting algorithm, Control Envelope Synthesis via Angelic Refinements (CESAR), is demonstrated in a range of safe control synthesis examples with different control challenges. △ Less

Submitted 4 April, 2024; v1 submitted 5 November, 2023; originally announced November 2023.

A Usage-Aware Sequent Calculus for Differential Dynamic Logic

Authors: Myra Dotzel, Stefan Mitsch, Andre Platzer

Abstract: Modeling languages like differential dynamic logic (dL) have proof calculi capable of proving guarantees for safety-critical applications. However, dL programmers may unintentionally over-specify assumptions and program statements, which results in overly constrained models, and consequently, weak or vacuous guarantees. In hybrid systems models, such constraints come from multiple places, ranging… ▽ More Modeling languages like differential dynamic logic (dL) have proof calculi capable of proving guarantees for safety-critical applications. However, dL programmers may unintentionally over-specify assumptions and program statements, which results in overly constrained models, and consequently, weak or vacuous guarantees. In hybrid systems models, such constraints come from multiple places, ranging from initial conditions to domain constraints in the middle of differential equations, thereby making it nontrivial to consistently track the conglomerate. We present a novel sequent calculus for dL that tracks which constraints to weaken or remove while preserving correctness guarantees. When properties follow entirely from constraints uninfluenced by program statements, this analysis spots outright flaws in models. We prove soundness and completeness of our proof calculus. △ Less

Submitted 6 September, 2023; v1 submitted 3 September, 2023; originally announced September 2023.

Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs

Authors: Marvin Brieger, Stefan Mitsch, André Platzer

Abstract: 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. Instantiations can be recovered from a single proof rule responsible for soundness-critical instantiation checks rather than being spread across axiom schemata in s… ▽ More 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. Instantiations can be recovered from a single proof rule responsible for soundness-critical instantiation checks rather than being spread across axiom schemata in side conditions. Even though communication and parallelism reasoning are notorious for necessitating subtle soundness-critical side conditions, uniform substitution when generalized to $\mathsf{dL}_\text{CHP}$ manages to limit and isolate their conceptual overhead. Since uniform substitution has proven to simplify the implementation of hybrid systems provers substantially, uniform substitution for $\mathsf{dL}_\text{CHP}$ paves the way for a parsimonious implementation of theorem provers for hybrid systems with communication and parallelism. △ Less

Submitted 18 July, 2023; v1 submitted 30 March, 2023; originally announced March 2023.

Comments: CADE 2023

ACM Class: F.3.1; F.4.1; D.2.4; C.1.m; C.2.4; D.4.7

Journal ref: International Conference on Automated Deduction, CADE-29 2023

Dynamic Logic of Communicating Hybrid Programs

Authors: Marvin Brieger, Stefan Mitsch, André Platzer

Abstract: This paper presents a dynamic logic $d\mathcal{L}_\text{CHP}$ for compositional deductive verification of communicating hybrid programs (CHPs). CHPs go beyond the traditional mixed discrete and continuous dynamics of hybrid systems by adding CSP-style operators for communication and parallelism. A compositional proof calculus is presented that modularly verifies CHPs including their parallel compo… ▽ More This paper presents a dynamic logic $d\mathcal{L}_\text{CHP}$ for compositional deductive verification of communicating hybrid programs (CHPs). CHPs go beyond the traditional mixed discrete and continuous dynamics of hybrid systems by adding CSP-style operators for communication and parallelism. A compositional proof calculus is presented that modularly verifies CHPs including their parallel compositions from proofs of their subprograms by assumption-commitment reasoning in dynamic logic. Unlike Hoare-style assumption-commitments, $d\mathcal{L}_\text{CHP}$ supports intuitive symbolic execution via explicit recorder variables for communication primitives. Since $d\mathcal{L}_\text{CHP}$ is a conservative extension of differential dynamic logic $d\mathcal{L}$, it can be used soundly along with the $d\mathcal{L}$ proof calculus and $d\mathcal{L}$'s complete axiomatization for differential equation invariants. △ Less

Submitted 3 March, 2023; v1 submitted 28 February, 2023; originally announced February 2023.

ACM Class: F.3.1; F.4.1; D.2.4; C.1.m; C.2.4; D.4.7

Differential Elimination and Algebraic Invariants of Polynomial Dynamical Systems

Authors: William Simmons, André Platzer

Abstract: Invariant sets are a key ingredient for verifying safety and other properties of cyber-physical systems that mix discrete and continuous dynamics. We adapt the elimination-theoretic Rosenfeld-Gröbner algorithm to systematically obtain algebraic invariants of polynomial dynamical systems without using Gröbner bases or quantifier elimination. We identify totally real varieties as an important class… ▽ More Invariant sets are a key ingredient for verifying safety and other properties of cyber-physical systems that mix discrete and continuous dynamics. We adapt the elimination-theoretic Rosenfeld-Gröbner algorithm to systematically obtain algebraic invariants of polynomial dynamical systems without using Gröbner bases or quantifier elimination. We identify totally real varieties as an important class for efficient invariance checking. △ Less

Submitted 25 January, 2023; originally announced January 2023.

A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL

Authors: Katherine Kosaian, Yong Kiam Tan, André Platzer

Abstract: We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula in the first-order logic of real arithmetic to a logically equivalent quantifier-free formula. The algorithm we formalize is a hybrid mixture of Tarski's original QE algorithm and the Ben-Or, Kozen, and Reif algorithm,… ▽ More We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula in the first-order logic of real arithmetic to a logically equivalent quantifier-free formula. The algorithm we formalize is a hybrid mixture of Tarski's original QE algorithm and the Ben-Or, Kozen, and Reif algorithm, and it is the first complete multivariate QE algorithm formalized in Isabelle/HOL. △ Less

Submitted 20 December, 2022; v1 submitted 22 September, 2022; originally announced September 2022.

Comments: CPP 2023

MSC Class: 68V20; 68V15; 03C10; 03B35; 03B10 ACM Class: F.3.1; F.4.1

Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis

Authors: Jonathan Laurent, André Platzer

Abstract: We propose a new approach to automated theorem proving where an AlphaZero-style agent is self-training to refine a generic high-level expert strategy expressed as a nondeterministic program. An analogous teacher agent is self-training to generate tasks of suitable relevance and difficulty for the learner. This allows leveraging minimal amounts of domain knowledge to tackle problems for which train… ▽ More We propose a new approach to automated theorem proving where an AlphaZero-style agent is self-training to refine a generic high-level expert strategy expressed as a nondeterministic program. An analogous teacher agent is self-training to generate tasks of suitable relevance and difficulty for the learner. This allows leveraging minimal amounts of domain knowledge to tackle problems for which training data is unavailable or hard to synthesize. As a specific illustration, we consider loop invariant synthesis for imperative programs and use neural networks to refine both the teacher and solver strategies. △ Less

Submitted 17 October, 2022; v1 submitted 27 May, 2022; originally announced May 2022.

Journal ref: Advances in Neural Information Processing Systems, volume 35 (2022) 4843--4856

Implicit Definitions with Differential Equations for KeYmaera X (System Description)

Authors: James Gallicchio, Yong Kiam Tan, Stefan Mitsch, André Platzer

Abstract: Definition packages in theorem provers provide users with means of defining and organizing concepts of interest. This system description presents a new definition package for the hybrid systems theorem prover KeYmaera X based on differential dynamic logic (dL). The package adds KeYmaera X support for user-defined smooth functions whose graphs can be implicitly characterized by dL formulas. Notably… ▽ More Definition packages in theorem provers provide users with means of defining and organizing concepts of interest. This system description presents a new definition package for the hybrid systems theorem prover KeYmaera X based on differential dynamic logic (dL). The package adds KeYmaera X support for user-defined smooth functions whose graphs can be implicitly characterized by dL formulas. Notably, this makes it possible to implicitly characterize functions, such as the exponential and trigonometric functions, as solutions of differential equations and then prove properties of those functions using dL's differential equation reasoning principles. Trustworthiness of the package is achieved by minimally extending KeYmaera X's soundness-critical kernel with a single axiom scheme that expands function occurrences with their implicit characterization. Users are provided with a high-level interface for defining functions and non-soundness-critical tactics that automate low-level reasoning over implicit characterizations in hybrid system proofs. △ Less

Submitted 31 May, 2022; v1 submitted 2 March, 2022; originally announced March 2022.

Comments: Long version of paper at IJCAR 2022 (11th International Joint Conference on Automated Reasoning, August 8-10, 2022, Haifa, Israel)

MSC Class: 03B70; 26E05; 33-04; 34A38 ACM Class: F.3.1; F.4.1; G.1.7; I.2.3

First-Order Game Logic and Modal Mu-Calculus

Authors: Noah Abou El Wafa, André Platzer

Abstract: This paper investigates first-order game logic and first-order modal mu-calculus, which extend their propositional modal logic counterparts with first-order modalities of interpreted effects such as variable assignments. Unlike in the propositional case, both logics are shown to have the same expressive power and their proof calculi to have the same deductive power. Both calculi are also mutually… ▽ More This paper investigates first-order game logic and first-order modal mu-calculus, which extend their propositional modal logic counterparts with first-order modalities of interpreted effects such as variable assignments. Unlike in the propositional case, both logics are shown to have the same expressive power and their proof calculi to have the same deductive power. Both calculi are also mutually relatively complete. In the presence of differential equations, corollaries obtain usable and complete translations between differential game logic, a logic for the deductive verification of hybrid games, and the differential mu-calculus, the modal mu-calculus for hybrid systems. The differential mu-calculus is complete with respect to first-order fixpoint logic and differential game logic is complete with respect to its ODE-free fragment. △ Less

Submitted 11 February, 2022; v1 submitted 24 January, 2022; originally announced January 2022.

MSC Class: 03B70; 03F03; 34A38; 91A25 ACM Class: F.3.1; F.4.1

Verifying Switched System Stability With Logic

Authors: Yong Kiam Tan, Stefan Mitsch, André Platzer

Abstract: 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 approach for verifying switched system stability that blends classical ideas from the controls and verification literature using differential dynamic logic (dL),… ▽ More 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 approach for verifying switched system stability that blends classical ideas from the controls and verification literature using differential dynamic logic (dL), a logic for deductive verification of hybrid systems. From controls, we use standard stability notions for various classes of switching mechanisms and their corresponding Lyapunov function-based analysis techniques. From verification, we use dL's ability to verify quantified properties of hybrid systems and dL models of switched systems as loo** hybrid programs whose stability can be formally specified and proven by finding appropriate loop invariants, i.e., properties that are preserved across each loop iteration. This blend of ideas enables a trustworthy implementation of switched system stability verification in the KeYmaera X prover based on dL. For standard classes of switching mechanisms, the implementation provides fully automated stability proofs, including searching for suitable Lyapunov functions. Moreover, the generality of the deductive approach also enables verification of switching control laws that require non-standard stability arguments through the design of loop invariants that suitably express specific intuitions behind those control laws. This flexibility is demonstrated on three case studies: a model for longitudinal flight control by Branicky, an automatic cruise controller, and Brockett's nonholonomic integrator. △ Less

Submitted 8 April, 2022; v1 submitted 2 November, 2021; originally announced November 2021.

Comments: Long version of paper at HSCC 2022 (25th ACM International Conference on Hybrid Systems: Computation and Control, May 4-6, 2022)

MSC Class: 03B70; 34A38; 93C30 ACM Class: F.3.1; F.4.1; G.1.7; I.2.3

Structured Proofs for Adversarial Cyber-Physical Systems

Authors: Rose Bohrer, André Platzer

Abstract: Many cyber-physical systems (CPS) are safety-critical, so it is important to formally verify them, e.g. in formal logics that show a model's correctness specification always holds. Constructive Differential Game Logic (CdGL) is such a logic for (constructive) hybrid games, including hybrid systems. To overcome undecidability, the user first writes a proof, for which we present a proof-checking t… ▽ More Many cyber-physical systems (CPS) are safety-critical, so it is important to formally verify them, e.g. in formal logics that show a model's correctness specification always holds. Constructive Differential Game Logic (CdGL) is such a logic for (constructive) hybrid games, including hybrid systems. To overcome undecidability, the user first writes a proof, for which we present a proof-checking tool. We introduce Kaisar, the first language and tool for CdGL proofs, which until now could only be written by hand with a low-level proof calculus. Kaisar's structured proofs simplify challenging CPS proof tasks, especially by using programming language principles and high-level stateful reasoning. Kaisar exploits CdGL's constructivity and refinement relations to build proofs around models of game strategies. The evaluation reproduces and extends existing case studies on 1D and 2D driving. Proof metrics are compared and reported experiences are discussed for the original studies and their reproductions. △ Less

Submitted 19 July, 2021; originally announced July 2021.

Comments: Preprint of paper appearing in ESWEEK-TECS (EMSOFT 2021)

Journal ref: ACM Trans. Embed. Comput. Syst. 20(5s), 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.

MSC Class: 03B70; 68Q60 ACM Class: F.3.1; C.3

Journal ref: ACM Trans. Embed. Comput. Syst. 22(1), pp. 10:1-10:30, 2023

Verified Quadratic Virtual Substitution for Real Arithmetic

Authors: Matias Scharager, Katherine Cordwell, Stefan Mitsch, André Platzer

Abstract: This paper presents a formally verified quantifier elimination (QE) algorithm for first-order real arithmetic by linear and quadratic virtual substitution (VS) in Isabelle/HOL. The Tarski-Seidenberg theorem established that the first-order logic of real arithmetic is decidable by QE. However, in practice, QE algorithms are highly complicated and often combine multiple methods for performance. VS i… ▽ More This paper presents a formally verified quantifier elimination (QE) algorithm for first-order real arithmetic by linear and quadratic virtual substitution (VS) in Isabelle/HOL. The Tarski-Seidenberg theorem established that the first-order logic of real arithmetic is decidable by QE. However, in practice, QE algorithms are highly complicated and often combine multiple methods for performance. VS is a practically successful method for QE that targets formulas with low-degree polynomials. To our knowledge, this is the first work to formalize VS for quadratic real arithmetic including inequalities. The proofs necessitate various contributions to the existing multivariate polynomial libraries in Isabelle/HOL. Our framework is modularized and easily expandable (to facilitate integrating future optimizations), and could serve as a basis for develo** practical general-purpose QE algorithms. Further, as our formalization is designed with practicality in mind, we export our development to SML and test the resulting code on 378 benchmarks from the literature, comparing to Redlog, Z3, Wolfram Engine, and SMT-RAT. This identified inconsistencies in some tools, underscoring the significance of a verified approach for the intricacies of real arithmetic. △ Less

Submitted 21 November, 2021; v1 submitted 28 May, 2021; originally announced May 2021.

Comments: FM 2021

MSC Class: 03B35; 03C10; 68V20 ACM Class: F.3.1; F.4.1

A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm

Authors: Katherine Cordwell, Yong Kiam Tan, André Platzer

Abstract: We formalize the univariate fragment of Ben-Or, Kozen, and Reif's (BKR) decision procedure for first-order real arithmetic in Isabelle/HOL. BKR's algorithm has good potential for parallelism and was designed to be used in practice. Its key insight is a clever recursive procedure that computes the set of all consistent sign assignments for an input set of univariate polynomials while carefully mana… ▽ More We formalize the univariate fragment of Ben-Or, Kozen, and Reif's (BKR) decision procedure for first-order real arithmetic in Isabelle/HOL. BKR's algorithm has good potential for parallelism and was designed to be used in practice. Its key insight is a clever recursive procedure that computes the set of all consistent sign assignments for an input set of univariate polynomials while carefully managing intermediate steps to avoid exponential blowup from naively enumerating all possible sign assignments (this insight is fundamental for both the univariate case and the general case). Our proof combines ideas from BKR and a follow-up work by Renegar that are well-suited for formalization. The resulting proof outline allows us to build substantially on Isabelle/HOL's libraries for algebra, analysis, and matrices. Our main extensions to existing libraries are also detailed. △ Less

Submitted 18 May, 2021; v1 submitted 5 February, 2021; originally announced February 2021.

Comments: ITP 2021

MSC Class: 68V20; 03C10 ACM Class: F.3.1

Switched Systems as Hybrid Programs

Authors: Yong Kiam Tan, André Platzer

Abstract: 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, e.g., using impulsive differential equations and switching, to automata-theoretic and language-based approaches. This paper bridges two such formalisms by showin… ▽ More 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, e.g., using impulsive differential equations and switching, to automata-theoretic and language-based approaches. This paper bridges two such formalisms by showing how various classes of switched systems can be modeled using the language of hybrid programs from differential dynamic logic (dL). The resulting models enable the formal specification and verification of switched systems using dL and its existing deductive verification tools such as KeYmaera X. Switched systems also provide a natural avenue for the generalization of dL's deductive proof theory for differential equations. The completeness results for switched system invariants proved in this paper enable effective safety verification of those systems in dL. △ Less

Submitted 29 April, 2021; v1 submitted 15 January, 2021; originally announced January 2021.

Comments: Long version of paper at ADHS 2021 (7th IFAC Conference on Analysis and Design of Hybrid Systems, July 7-9, 2021)

MSC Class: 03B70; 34A38; 93C30 ACM Class: F.3.1; F.4.1; G.1.7; I.2.3

Deductive Stability Proofs for Ordinary Differential Equations

Authors: Yong Kiam Tan, André Platzer

Abstract: Stability is required for real world controlled systems as it ensures that those systems can tolerate small, real world perturbations around their desired operating states. This paper shows how stability for continuous systems modeled by ordinary differential equations (ODEs) can be formally verified in differential dynamic logic (dL). The key insight is to specify ODE stability by suitably nestin… ▽ More Stability is required for real world controlled systems as it ensures that those systems can tolerate small, real world perturbations around their desired operating states. This paper shows how stability for continuous systems modeled by ordinary differential equations (ODEs) can be formally verified in differential dynamic logic (dL). The key insight is to specify ODE stability by suitably nesting the dynamic modalities of dL with first-order logic quantifiers. Elucidating the logical structure of stability properties in this way has three key benefits: i) it provides a flexible means of formally specifying various stability properties of interest, ii) it yields rigorous proofs of those stability properties from dL's axioms with dL's ODE safety and liveness proof principles, and iii) it enables formal analysis of the relationships between various stability properties which, in turn, inform proofs of those properties. These benefits are put into practice through an implementation of stability proofs for several examples in KeYmaera X, a hybrid systems theorem prover based on dL. △ Less

Submitted 23 February, 2022; v1 submitted 25 October, 2020; originally announced October 2020.

Comments: Long version of paper at TACAS 2021 (27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 27 Mar - 1 Apr 2021)

MSC Class: 03B70; 34A38; 34D05; 93D05 ACM Class: F.3.1; F.4.1; G.1.7; I.2.3

Pegasus: Sound Continuous Invariant Generation

Authors: Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer

Abstract: Continuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without having to unroll their loops, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the b… ▽ More Continuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without having to unroll their loops, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges to the automation of formal proofs of safety for hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks. △ Less

Submitted 17 September, 2020; v1 submitted 19 May, 2020; originally announced May 2020.

Comments: Extended version of FM'19 conference paper (https://doi.org/10.1007/978-3-030-30942-8_10), to appear in FMSD

ACM Class: F.3.1; F.4.1; G.4; I.1

An Axiomatic Approach to Existence and Liveness for Differential Equations

Authors: Yong Kiam Tan, André Platzer

Abstract: This article presents an axiomatic approach for deductive verification of existence and liveness for ordinary differential equations (ODEs) with differential dynamic logic (dL). The approach yields proofs that the solution of a given ODE exists long enough to reach a given target region without leaving a given evolution domain. Numerous subtleties complicate the generalization of discrete liveness… ▽ More This article presents an axiomatic approach for deductive verification of existence and liveness for ordinary differential equations (ODEs) with differential dynamic logic (dL). The approach yields proofs that the solution of a given ODE exists long enough to reach a given target region without leaving a given evolution domain. Numerous subtleties complicate the generalization of discrete liveness verification techniques, such as loop variants, to the continuous setting. For example, ODE solutions may blow up in finite time or their progress towards the goal may converge to zero. These subtleties are handled in dL by successively refining ODE liveness properties using ODE invariance properties which have a complete axiomatization. This approach is widely applicable: several liveness arguments from the literature are surveyed and derived as special instances of axiomatic refinement in dL. These derivations also correct several soundness errors in the surveyed literature, which further highlights the subtlety of ODE liveness reasoning and the utility of an axiomatic approach. An important special case of this approach deduces (global) existence properties of ODEs, which are a fundamental part of every ODE liveness argument. Thus, all generalizations of existence properties and their proofs immediately lead to corresponding generalizations of ODE liveness arguments. Overall, the resulting library of common refinement steps enables both the sound development and justification of new ODE existence and of liveness proof rules from dL axioms. These insights are put into practice through an implementation of ODE liveness proofs in the KeYmaera X theorem prover for hybrid systems. △ Less

Submitted 9 August, 2020; v1 submitted 29 April, 2020; originally announced April 2020.

Comments: Significantly extended version of arXiv:1904.07984

MSC Class: 03B70; 34A38 ACM Class: F.3.1; F.4.1; G.1.7; I.2.3

Journal ref: Formal Aspects of Computing 33, pp. 461-518, 2021

Constructive Game Logic

Authors: Rose Bohrer, André Platzer

Abstract: Game Logic is an excellent setting to study proofs-about-programs via the interpretation of those proofs as programs, because constructive proofs for games correspond to effective winning strategies to follow in response to the opponent's actions. We thus develop Constructive Game Logic which extends Parikh's Game Logic (GL) with constructivity and with first-order programs a la Pratt's first-or… ▽ More Game Logic is an excellent setting to study proofs-about-programs via the interpretation of those proofs as programs, because constructive proofs for games correspond to effective winning strategies to follow in response to the opponent's actions. We thus develop Constructive Game Logic which extends Parikh's Game Logic (GL) with constructivity and with first-order programs a la Pratt's first-order dynamic logic (DL). Our major contributions include: 1) a novel realizability semantics capturing the adversarial dynamics of games, 2) a natural deduction calculus and operational semantics describing the computational meaning of strategies via proof-terms, and 3) theoretical results including soundness of the proof calculus w.r.t. realizability semantics, progress and preservation of the operational semantics of proofs, and Existence Properties on support of the extraction of computational artifacts from game proofs. Together, these results provide the most general account of a Curry-Howard interpretation for any program logic to date, and the first at all for Game Logic. △ Less

Submitted 22 July, 2020; v1 submitted 19 February, 2020; originally announced February 2020.

Comments: 74 pages, extended preprint for ESOP

Refining Constructive Hybrid Games

Authors: Rose Bohrer, André Platzer

Abstract: We extend the constructive differential game logic (CdGL) of hybrid games with a refinement connective that relates two hybrid games. We use this connective to prove a folk theorem relating hybrid games to hybrid systems. We extend the constructive differential game logic (CdGL) of hybrid games with a refinement connective that relates two hybrid games. We use this connective to prove a folk theorem relating hybrid games to hybrid systems. △ Less

Submitted 13 February, 2020; v1 submitted 6 February, 2020; originally announced February 2020.

Comments: 40 pages. Extended preprint

Constructive Hybrid Games

Authors: Rose Bohrer, André Platzer

Abstract: Hybrid games are models which combine discrete, continuous, and adversarial dynamics. Game logic enables proving (classical) existence of winning strategies. We introduce constructive differential game logic (CdGL) for hybrid games, where proofs that a player can win the game correspond to computable winning strategies. This is the logical foundation for synthesis of correct control and monitori… ▽ More Hybrid games are models which combine discrete, continuous, and adversarial dynamics. Game logic enables proving (classical) existence of winning strategies. We introduce constructive differential game logic (CdGL) for hybrid games, where proofs that a player can win the game correspond to computable winning strategies. This is the logical foundation for synthesis of correct control and monitoring code for safety-critical cyber-physical systems. Our contributions include novel static and dynamic semantics as well as soundness and consistency. △ Less

Submitted 6 February, 2020; originally announced February 2020.

Comments: 60 pages, preprint, under review

A Positive Mass Theorem for Static Causal Fermion Systems

Authors: Felix Finster, Andreas Platzer

Abstract: Asymptotically flat static causal fermion systems are introduced. Their total mass is defined as a limit of surface layer integrals which compare the measures describing the asymptotically flat spacetime and a vacuum spacetime near spatial infinity. Our definition does not involve any regularity assumptions; it even applies to singular or generalized "quantum" spacetimes. A positive mass theorem i… ▽ More Asymptotically flat static causal fermion systems are introduced. Their total mass is defined as a limit of surface layer integrals which compare the measures describing the asymptotically flat spacetime and a vacuum spacetime near spatial infinity. Our definition does not involve any regularity assumptions; it even applies to singular or generalized "quantum" spacetimes. A positive mass theorem is proven. Our methods and results explain why and how the causal action principle incorporates the nonlinear effects of gravity for static systems. △ Less

Submitted 12 October, 2023; v1 submitted 30 December, 2019; originally announced December 2019.

Comments: 57 pages, LaTeX, 3 figures, sign errors in (6.5) and (6.9) corrected, footnote on page 43 added

Journal ref: Adv.Theor.Math.Phys. 25 (2021) 1735-1818

Overview of Logical Foundations of Cyber-Physical Systems

Authors: André Platzer

Abstract: Cyber-physical systems (CPSs) are important whenever computer technology interfaces with the physical world as it does in self-driving cars or aircraft control support systems. Due to their many subtleties, controllers for cyber-physical systems deserve to be held to the highest correctness standards. Their correct functioning is crucial, which explains the broad interest in safety analysis techno… ▽ More Cyber-physical systems (CPSs) are important whenever computer technology interfaces with the physical world as it does in self-driving cars or aircraft control support systems. Due to their many subtleties, controllers for cyber-physical systems deserve to be held to the highest correctness standards. Their correct functioning is crucial, which explains the broad interest in safety analysis technology for their mathematical models, which are called hybrid systems because they combine discrete dynamics with continuous dynamics. Differential dynamic logic (dL) provides logical specification and rigorous reasoning techniques for hybrid systems. The logic dL is implemented in the theorem prover KeYmaera X, which has been instrumental in verifying ground robot controllers, railway systems, and the next-generation airborne collision avoidance system ACAS X. This chapter provides an informal overview of this logical approach to CPS safety that is detailed in a recent textbook on Logical Foundations of Cyber-Physical Systems. It also explains how safety guarantees obtained in the land of verified models reach the level of CPS execution unharmed. △ Less

Submitted 24 October, 2019; originally announced October 2019.

Report number: In Helmut Seidl, editor, Post-proceedings of the Summer School Marktoberdorf: Safety and Security of Software Systems - Logics, Proofs, Applications, TUM University Press, 2020 MSC Class: 03B70; 34A38 ACM Class: F.4.1; F.3.1; F.3.2; I.2.3

Toward Structured Proofs for Dynamic Logics

Authors: Rose Bohrer, André Platzer

Abstract: We present Kaisar, a structured interactive proof language for differential dynamic logic (dL), for safety-critical cyber-physical systems (CPS). The defining feature of Kaisar is *nominal terms*, which simplify CPS proofs by making the frequently needed historical references to past program states first-class. To support nominals, we extend the notion of structured proof with a first-class noti… ▽ More We present Kaisar, a structured interactive proof language for differential dynamic logic (dL), for safety-critical cyber-physical systems (CPS). The defining feature of Kaisar is *nominal terms*, which simplify CPS proofs by making the frequently needed historical references to past program states first-class. To support nominals, we extend the notion of structured proof with a first-class notion of *structured symbolic execution* of CPS models. We implement Kaisar in the theorem prover KeYmaera X and reproduce an example on the safe operation of a parachute and a case study on ground robot control. We show how nominals simplify common CPS reasoning tasks when combined with other features of structured proof. We develop an extensive metatheory for Kaisar. In addition to soundness and completeness, we show a formal specification for Kaisar's nominals and relate Kaisar to a nominal variant of dL. △ Less

Submitted 15 August, 2019; originally announced August 2019.

Differential Equation Invariance Axiomatization

Authors: André Platzer, Yong Kiam Tan

Abstract: This article proves the completeness of an axiomatization for differential equation invariants described by Noetherian functions. First, the differential equation axioms of differential dynamic logic are shown to be complete for reasoning about analytic invariants. Completeness crucially exploits differential ghosts, which introduce additional variables that can be chosen to evolve freely along ne… ▽ More This article proves the completeness of an axiomatization for differential equation invariants described by Noetherian functions. First, the differential equation axioms of differential dynamic logic are shown to be complete for reasoning about analytic invariants. Completeness crucially exploits differential ghosts, which introduce additional variables that can be chosen to evolve freely along new differential equations. Cleverly chosen differential ghosts are the proof-theoretical counterpart of dark matter. They create new hypothetical state, whose relationship to the original state variables satisfies invariants that did not exist before. The reflection of these new invariants in the original system then enables its analysis. An extended axiomatization with existence and uniqueness axioms is complete for all local progress properties, and, with a real induction axiom, is complete for all semianalytic invariants. This parsimonious axiomatization serves as the logical foundation for reasoning about invariants of differential equations. Indeed, it is precisely this logical treatment that enables the generalization of completeness to the Noetherian case. △ Less

Submitted 7 February, 2020; v1 submitted 31 May, 2019; originally announced May 2019.

Comments: Significantly extended version of arXiv:1802.01226

MSC Class: F.4.1; F.3.1; G.1.7; I.2.3 ACM Class: F.4.1; F.3.1; G.1.7; I.2.3

Journal ref: J. ACM 67(1), Article 6, 2020, 66 pages

Towards Physical Hybrid Systems

Authors: Katherine Cordwell, André Platzer

Abstract: Some hybrid systems models are unsafe for mathematically correct but physically unrealistic reasons. For example, mathematical models can classify a system as being unsafe on a set that is too small to have physical importance. In particular, differences in measure zero sets in models of cyber-physical systems (CPS) have significant mathematical impact on the mathematical safety of these models ev… ▽ More Some hybrid systems models are unsafe for mathematically correct but physically unrealistic reasons. For example, mathematical models can classify a system as being unsafe on a set that is too small to have physical importance. In particular, differences in measure zero sets in models of cyber-physical systems (CPS) have significant mathematical impact on the mathematical safety of these models even though differences on measure zero sets have no tangible physical effect in a real system. We develop the concept of "physical hybrid systems" (PHS) to help reunite mathematical models with physical reality. We modify a hybrid systems logic (differential temporal dynamic logic) by adding a first-class operator to elide distinctions on measure zero sets of time within CPS models. This approach facilitates modeling since it admits the verification of a wider class of models, including some physically realistic models that would otherwise be classified as mathematically unsafe. We also develop a proof calculus to help with the verification of PHS. △ Less

Submitted 14 September, 2019; v1 submitted 23 May, 2019; originally announced May 2019.

Comments: CADE 2019

MSC Class: 03B70; 34A38 ACM Class: F.4.1; F.3.1

An Axiomatic Approach to Liveness for Differential Equations

Authors: Yong Kiam Tan, André Platzer

Abstract: This paper presents an approach for deductive liveness verification for ordinary differential equations (ODEs) with differential dynamic logic. Numerous subtleties complicate the generalization of well-known discrete liveness verification techniques, such as loop variants, to the continuous setting. For example, ODE solutions may blow up in finite time or their progress towards the goal may conver… ▽ More This paper presents an approach for deductive liveness verification for ordinary differential equations (ODEs) with differential dynamic logic. Numerous subtleties complicate the generalization of well-known discrete liveness verification techniques, such as loop variants, to the continuous setting. For example, ODE solutions may blow up in finite time or their progress towards the goal may converge to zero. Our approach handles these subtleties by successively refining ODE liveness properties using ODE invariance properties which have a well-understood deductive proof theory. This approach is widely applicable: we survey several liveness arguments in the literature and derive them all as special instances of our axiomatic refinement approach. We also correct several soundness errors in the surveyed arguments, which further highlights the subtlety of ODE liveness reasoning and the utility of our deductive approach. The library of common refinement steps identified through our approach enables both the sound development and justification of new ODE liveness proof rules from our axioms. △ Less

Submitted 10 July, 2019; v1 submitted 16 April, 2019; originally announced April 2019.

Comments: FM 2019: 23rd International Symposium on Formal Methods, Porto, Portugal, October 9-11, 2019

MSC Class: 03B70; 34A38 ACM Class: F.3.1; F.4.1; G.1.7; I.2.3

A Formal Safety Net for Waypoint Following in Ground Robots

Authors: Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Andrew Sogokon, André Platzer

Abstract: We present a reusable formally verified safety net that provides end-to-end safety and liveness guarantees for 2D waypoint-following of Dubins-type ground robots with tolerances and acceleration. We: i) Model a robot in differential dynamic logic (dL), and specify assumptions on the controller and robot kinematics, ii) Prove formal safety and liveness properties for waypoint-following with speed l… ▽ More We present a reusable formally verified safety net that provides end-to-end safety and liveness guarantees for 2D waypoint-following of Dubins-type ground robots with tolerances and acceleration. We: i) Model a robot in differential dynamic logic (dL), and specify assumptions on the controller and robot kinematics, ii) Prove formal safety and liveness properties for waypoint-following with speed limits, iii) Synthesize a monitor, which is automatically proven to enforce model compliance at runtime, and iv) Our use of the VeriPhy toolchain makes these guarantees carry over down to the level of machine code with untrusted controllers, environments, and plans. The guarantees for the safety net apply to any robot as long as the waypoints are chosen safely and the physical assumptions in its model hold. Experiments show these assumptions hold in practice, with an inherent trade-off between compliance and performance. △ Less

Submitted 18 June, 2019; v1 submitted 12 March, 2019; originally announced March 2019.

MSC Class: 03B70; 34A38; 68Q60; 93C85 ACM Class: I.2.9; D.2.4; F.3.1; C.3

Uniform Substitution At One Fell Swoop

Authors: André Platzer

Abstract: Uniform substitution of function, predicate, program or game symbols is the core operation in parsimonious provers for hybrid systems and hybrid games. By postponing soundness-critical admissibility checks, this paper introduces a uniform substitution mechanism that proceeds in a linear pass homomorphically along the formula. Soundness is recovered using a simple variable condition at the replacem… ▽ More Uniform substitution of function, predicate, program or game symbols is the core operation in parsimonious provers for hybrid systems and hybrid games. By postponing soundness-critical admissibility checks, this paper introduces a uniform substitution mechanism that proceeds in a linear pass homomorphically along the formula. Soundness is recovered using a simple variable condition at the replacements performed by the substitution. The setting in this paper is that of differential hybrid games, in which discrete, continuous, and adversarial dynamics interact in differential game logic dGL. This paper proves soundness and completeness of one-pass uniform substitutions for dGL. △ Less

Submitted 22 May, 2019; v1 submitted 19 February, 2019; originally announced February 2019.

Comments: CADE 2019 Extending arXiv:1804.05880 with differential games arXiv:1507.04943

MSC Class: 03F03; 03B70; 34A38; 91A25 ACM Class: F.4.1; F.3.1; F.3.2; I.2.3

Verifiably Safe Off-Model Reinforcement Learning

Authors: Nathan Fulton, Andre Platzer

Abstract: The desire to use reinforcement learning in safety-critical settings has inspired a recent interest in formal methods for learning algorithms. Existing formal methods for learning and optimization primarily consider the problem of constrained learning or constrained optimization. Given a single correct model and associated safety constraint, these approaches guarantee efficient learning while prov… ▽ More The desire to use reinforcement learning in safety-critical settings has inspired a recent interest in formal methods for learning algorithms. Existing formal methods for learning and optimization primarily consider the problem of constrained learning or constrained optimization. Given a single correct model and associated safety constraint, these approaches guarantee efficient learning while provably avoiding behaviors outside the safety constraint. Acting well given an accurate environmental model is an important pre-requisite for safe learning, but is ultimately insufficient for systems that operate in complex heterogeneous environments. This paper introduces verification-preserving model updates, the first approach toward obtaining formal safety guarantees for reinforcement learning in settings where multiple environmental models must be taken into account. Through a combination of design-time model updates and runtime model falsification, we provide a first approach toward obtaining formal safety proofs for autonomous systems acting in heterogeneous environments. △ Less

Submitted 14 February, 2019; originally announced February 2019.

Comments: TACAS 2019

HyPLC: Hybrid Programmable Logic Controller Program Translation for Verification

Authors: Luis Garcia, Stefan Mitsch, Andre Platzer

Abstract: Programmable Logic Controllers (PLCs) provide a prominent choice of implementation platform for safety-critical industrial control systems. Formal verification provides ways of establishing correctness guarantees, which can be quite important for such safety-critical applications. But since PLC code does not include an analytic model of the system plant, their verification is limited to discrete p… ▽ More Programmable Logic Controllers (PLCs) provide a prominent choice of implementation platform for safety-critical industrial control systems. Formal verification provides ways of establishing correctness guarantees, which can be quite important for such safety-critical applications. But since PLC code does not include an analytic model of the system plant, their verification is limited to discrete properties. In this paper, we, thus, start the other way around with hybrid programs that include continuous plant models in addition to discrete control algorithms. Even deep correctness properties of hybrid programs can be formally verified in the theorem prover KeYmaera X that implements differential dynamic logic, dL, for hybrid programs. After verifying the hybrid program, we now present an approach for translating hybrid programs into PLC code. The new tool, HyPLC, implements this translation of discrete control code of verified hybrid program models to PLC controller code and, vice versa, the translation of existing PLC code into the discrete control actions for a hybrid program given an additional input of the continuous dynamics of the system to be verified. This approach allows for the generation of real controller code while preserving, by compilation, the correctness of a valid and verified hybrid program. PLCs are common cyber-physical interfaces for safety-critical industrial control applications, and HyPLC serves as a pragmatic tool for bridging formal verification of complex cyber-physical systems at the algorithmic level of hybrid programs with the execution layer of concrete PLC implementations. △ Less

Submitted 13 February, 2019; originally announced February 2019.

Comments: 13 pages, 9 figures. ICCPS 2019

Verified Runtime Validation for Partially Observable Hybrid Systems

Authors: Stefan Mitsch, André Platzer

Abstract: Formal verification provides strong safety guarantees but only for models of cyber-physical systems. Hybrid system models describe the required interplay of computation and physical dynamics, which is crucial to guarantee what computations lead to safe physical behavior (e.g., cars should not collide). Control computations that affect physical dynamics must act in advance to avoid possibly unsafe… ▽ More Formal verification provides strong safety guarantees but only for models of cyber-physical systems. Hybrid system models describe the required interplay of computation and physical dynamics, which is crucial to guarantee what computations lead to safe physical behavior (e.g., cars should not collide). Control computations that affect physical dynamics must act in advance to avoid possibly unsafe future circumstances. Formal verification then ensures that the controllers correctly identify and provably avoid unsafe future situations under a certain model of physics. But any model of physics necessarily deviates from reality and, moreover, any observation with real sensors and manipulation with real actuators is subject to uncertainty. This makes runtime validation a crucial step to monitor whether the model assumptions hold for the real system implementation. The key question is what property needs to be runtime-monitored and what a satisfied runtime monitor entails about the safety of the system: the observations of a runtime monitor only relate back to the safety of the system if they are themselves accompanied by a proof of correctness! For an unbroken chain of correctness guarantees, we, thus, synthesize runtime monitors in a provably correct way from provably safe hybrid system models. This paper addresses the inevitable challenge of making the synthesized monitoring conditions robust to partial observability of sensor uncertainty and partial controllability due to actuator disturbance. We show that the monitoring conditions result in provable safety guarantees with fallback controllers that react to monitor violation at runtime. △ Less

Submitted 24 February, 2019; v1 submitted 15 November, 2018; originally announced November 2018.

ACM Class: F.4.1; I.2.2; J.2

Uniform Substitution for Differential Game Logic

Authors: André Platzer

Abstract: This paper presents a uniform substitution calculus for differential game logic (dGL). Church's uniform substitutions substitute a term or formula for a function or predicate symbol everywhere. After generalizing them to differential game logic and allowing for the substitution of hybrid games for game symbols, uniform substitutions make it possible to only use axioms instead of axiom schemata, th… ▽ More This paper presents a uniform substitution calculus for differential game logic (dGL). Church's uniform substitutions substitute a term or formula for a function or predicate symbol everywhere. After generalizing them to differential game logic and allowing for the substitution of hybrid games for game symbols, uniform substitutions make it possible to only use axioms instead of axiom schemata, thereby substantially simplifying implementations. Instead of subtle schema variables and soundness-critical side conditions on the occurrence patterns of logical variables to restrict infinitely many axiom schema instances to sound ones, the resulting axiomatization adopts only a finite number of ordinary dGL formulas as axioms, which uniform substitutions instantiate soundly. This paper proves soundness and completeness of uniform substitutions for the monotone modal logic dGL. The resulting axiomatization admits a straightforward modular implementation of dGL in theorem provers. △ Less

Submitted 16 April, 2018; originally announced April 2018.

MSC Class: 03F03; 03B70; 34A38; 91A25 ACM Class: F.4.1; F.3.1; F.3.2; I.2.3

Journal ref: Automated Reasoning, 9th International Joint Conference, IJCAR 2018

Differential Equation Axiomatization: The Impressive Power of Differential Ghosts

Authors: André Platzer, Yong Kiam Tan

Abstract: We prove the completeness of an axiomatization for differential equation invariants. First, we show that the differential equation axioms in differential dynamic logic are complete for all algebraic invariants. Our proof exploits differential ghosts, which introduce additional variables that can be chosen to evolve freely along new differential equations. Cleverly chosen differential ghosts are th… ▽ More We prove the completeness of an axiomatization for differential equation invariants. First, we show that the differential equation axioms in differential dynamic logic are complete for all algebraic invariants. Our proof exploits differential ghosts, which introduce additional variables that can be chosen to evolve freely along new differential equations. Cleverly chosen differential ghosts are the proof-theoretical counterpart of dark matter. They create new hypothetical state, whose relationship to the original state variables satisfies invariants that did not exist before. The reflection of these new invariants in the original system then enables its analysis. We then show that extending the axiomatization with existence and uniqueness axioms makes it complete for all local progress properties, and further extension with a real induction axiom makes it complete for all real arithmetic invariants. This yields a parsimonious axiomatization, which serves as the logical foundation for reasoning about invariants of differential equations. Moreover, our results are purely axiomatic, and so the axiomatization is suitable for sound implementation in foundational theorem provers. △ Less

Submitted 10 June, 2019; v1 submitted 4 February, 2018; originally announced February 2018.

Comments: LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, July 9-12, 2018, Oxford, United Kingdom, ACM ISBN 978-1-4503-5583-4/18/07

Report number: CMU-CS-17-117 MSC Class: 03B70; 03F03; 34C14; 34A38 ACM Class: F.4.1; F.3.1; G.1.7; I.2.3

KEGGexpressionMapper allows for analysis of pathways over multiple conditions by integrating transcriptomics and proteomics measurements

Authors: Thomas Nussbaumer, Julia Polzin, Alexander Platzer

Abstract: Motivation: In transcriptomic and proteomics-based studies, the abundance of genes is often compared to functional pathways such as the Kyoto Encyclopaedia at Genes and Genomes (KEGG) to identify active metabolic processes. Even though a plethora of tools allow to analyze and to compare omics data in respect to KEGG pathways, the analysis of multiple conditions is often limited to only a defined s… ▽ More Motivation: In transcriptomic and proteomics-based studies, the abundance of genes is often compared to functional pathways such as the Kyoto Encyclopaedia at Genes and Genomes (KEGG) to identify active metabolic processes. Even though a plethora of tools allow to analyze and to compare omics data in respect to KEGG pathways, the analysis of multiple conditions is often limited to only a defined set of conditions. Furthermore, for transcriptomic datasets, it is crucial to compare the entire set of pathways in order to obtain a global overview of the species' metabolic functions. Results: Here, we present the tool KEGGexpressionMapper, a module, that is implemented in the programming language R. The module allows to highlight the expression of transcriptomic or proteomic measurements in various conditions on pathways and incorporates methods to analyze gene enrichment analyses and expression clustering in time series data. KEGGexpressionMapper supports time series data from transcriptomic or proteomics measurements from different individuals. As the tool is implemented in the scripting language R, it can be integrated into existing analysis pipelines to obtain a global overview of the dataset. The R package can be downloaded from https://github.com/nthomasCUBE/KEGGexpressionmapper. △ Less

Submitted 24 August, 2017; originally announced August 2017.

Comments: 15 pages, 3 figures

The KeYmaera X Proof IDE - Concepts on Usability in Hybrid Systems Theorem Proving

Authors: Stefan Mitsch, André Platzer

Abstract: Hybrid systems verification is quite important for develo** correct controllers for physical systems, but is also challenging. Verification engineers, thus, need to be empowered with ways of guiding hybrid systems verification while receiving as much help from automation as possible. Due to undecidability, verification tools need sufficient means for intervening during the verification and need… ▽ More Hybrid systems verification is quite important for develo** correct controllers for physical systems, but is also challenging. Verification engineers, thus, need to be empowered with ways of guiding hybrid systems verification while receiving as much help from automation as possible. Due to undecidability, verification tools need sufficient means for intervening during the verification and need to allow verification engineers to provide system design insights. This paper presents the design ideas behind the user interface for the hybrid systems theorem prover KeYmaera X. We discuss how they make it easier to prove hybrid systems as well as help learn how to conduct proofs in the first place. Unsurprisingly, the most difficult user interface challenges come from the desire to integrate automation and human guidance. We also share thoughts how the success of such a user interface design could be evaluated and anecdotal observations about it. △ Less

Submitted 29 January, 2017; originally announced January 2017.

Comments: In Proceedings F-IDE 2016, arXiv:1701.07925

Journal ref: EPTCS 240, 2017, pp. 67-81

Formal Verification of Obstacle Avoidance and Navigation of Ground Robots

Authors: Stefan Mitsch, Khalil Ghorbal, David Vogelbacher, André Platzer

Abstract: The safety of mobile robots in dynamic environments is predicated on making sure that they do not collide with obstacles. In support of such safety arguments, we analyze and formally verify a series of increasingly powerful safety properties of controllers for avoiding both stationary and moving obstacles: (i) static safety, which ensures that no collisions can happen with stationary obstacles, (i… ▽ More The safety of mobile robots in dynamic environments is predicated on making sure that they do not collide with obstacles. In support of such safety arguments, we analyze and formally verify a series of increasingly powerful safety properties of controllers for avoiding both stationary and moving obstacles: (i) static safety, which ensures that no collisions can happen with stationary obstacles, (ii) passive safety, which ensures that no collisions can happen with stationary or moving obstacles while the robot moves, (iii) the stronger passive friendly safety in which the robot further maintains sufficient maneuvering distance for obstacles to avoid collision as well, and (iv) passive orientation safety, which allows for imperfect sensor coverage of the robot, i. e., the robot is aware that not everything in its environment will be visible. We complement these provably correct safety properties with liveness properties: we prove that provably safe motion is flexible enough to let the robot still navigate waypoints and pass intersections. We use hybrid system models and theorem proving techniques that describe and formally verify the robot's discrete control decisions along with its continuous, physical motion. Moreover, we formally prove that safety can still be guaranteed despite sensor uncertainty and actuator perturbation, and when control choices for more aggressive maneuvers are introduced. Our verification results are generic in the sense that they are not limited to the particular choices of one specific control algorithm but identify conditions that make them simultaneously apply to a broad class of control algorithms. △ Less

Submitted 18 June, 2019; v1 submitted 2 May, 2016; originally announced May 2016.

MSC Class: 03B70; 34A38; 68Q60 ACM Class: I.2.9; D.2.4; F.3.1; C.3

Journal ref: International Journal of Robotics Research. 36(12), pp. 1312-1340, 2017

A Complete Uniform Substitution Calculus for Differential Dynamic Logic

Authors: André Platzer

Abstract: This article introduces a relatively complete proof calculus for differential dynamic logic (dL) that is entirely based on uniform substitution, a proof rule that substitutes a formula for a predicate symbol everywhere. Uniform substitutions make it possible to use axioms instead of axiom schemata, thereby substantially simplifying implementations. Instead of subtle schema variables and soundness-… ▽ More This article introduces a relatively complete proof calculus for differential dynamic logic (dL) that is entirely based on uniform substitution, a proof rule that substitutes a formula for a predicate symbol everywhere. Uniform substitutions make it possible to use axioms instead of axiom schemata, thereby substantially simplifying implementations. Instead of subtle schema variables and soundness-critical side conditions on the occurrence patterns of logical variables to restrict infinitely many axiom schema instances to sound ones, the resulting calculus adopts only a finite number of ordinary dL formulas as axioms, which uniform substitutions instantiate soundly. The static semantics of differential dynamic logic and the soundness-critical restrictions it imposes on proof steps is captured exclusively in uniform substitutions and variable renamings as opposed to being spread in delicate ways across the prover implementation. In addition to sound uniform substitutions, this article introduces differential forms for differential dynamic logic that make it possible to internalize differential invariants, differential substitutions, and derivatives as first-class axioms to reason about differential equations axiomatically. The resulting axiomatization of differential dynamic logic is proved to be sound and relatively complete. △ Less

Submitted 27 July, 2016; v1 submitted 22 January, 2016; originally announced January 2016.

Comments: Long article extending the conference version that appeared at CADE 2015, arXiv:1503.01981

MSC Class: 03F03; 03B70; 34A38 ACM Class: F.4.1; F.3.1; F.3.2; I.2.3

Journal ref: Journal of Automated Reasoning, 59(2), pages 219-265, 2017

Forward Invariant Cuts to Simplify Proofs of Safety

Authors: Nikos Arechiga, James Kapinski, Jyotirmoy Deshmukh, Andre Platzer, Bruce Krogh

Abstract: The use of deductive techniques, such as theorem provers, has several advantages in safety verification of hybrid sys- tems; however, state-of-the-art theorem provers require ex- tensive manual intervention. Furthermore, there is often a gap between the type of assistance that a theorem prover requires to make progress on a proof task and the assis- tance that a system designer is able to provide.… ▽ More The use of deductive techniques, such as theorem provers, has several advantages in safety verification of hybrid sys- tems; however, state-of-the-art theorem provers require ex- tensive manual intervention. Furthermore, there is often a gap between the type of assistance that a theorem prover requires to make progress on a proof task and the assis- tance that a system designer is able to provide. This paper presents an extension to KeYmaera, a deductive verification tool for differential dynamic logic; the new technique allows local reasoning using system designer intuition about per- formance within particular modes as part of a proof task. Our approach allows the theorem prover to leverage for- ward invariants, discovered using numerical techniques, as part of a proof of safety. We introduce a new inference rule into the proof calculus of KeYmaera, the forward invariant cut rule, and we present a methodology to discover useful forward invariants, which are then used with the new cut rule to complete verification tasks. We demonstrate how our new approach can be used to complete verification tasks that lie out of the reach of existing deductive approaches us- ing several examples, including one involving an automotive powertrain control system. △ Less

Submitted 10 August, 2015; v1 submitted 17 July, 2015; originally announced July 2015.

Comments: Extended version of EMSOFT paper

Differential Hybrid Games

Authors: André Platzer

Abstract: This article introduces differential hybrid games, which combine differential games with hybrid games. In both kinds of games, two players interact with continuous dynamics. The difference is that hybrid games also provide all the features of hybrid systems and discrete games, but only deterministic differential equations. Differential games, instead, provide differential equations with continuous… ▽ More This article introduces differential hybrid games, which combine differential games with hybrid games. In both kinds of games, two players interact with continuous dynamics. The difference is that hybrid games also provide all the features of hybrid systems and discrete games, but only deterministic differential equations. Differential games, instead, provide differential equations with continuous-time game input by both players, but not the luxury of hybrid games, such as mode switches and discrete-time or alternating adversarial interaction. This article augments differential game logic with modalities for the combined dynamics of differential hybrid games. It shows how hybrid games subsume differential games and introduces differential game invariants and differential game variants for proving properties of differential games inductively. △ Less

Submitted 23 February, 2017; v1 submitted 17 July, 2015; originally announced July 2015.

Report number: CMU-CS-14-102 MSC Class: 03B70; 91A23; 34A38; 91A25; 03F03 ACM Class: F.3.1; F.4.1

Journal ref: ACM Transactions on Computational Logic 18(3), pages 19:1-19:44, 2017

A Uniform Substitution Calculus for Differential Dynamic Logic

Authors: André Platzer

Abstract: This paper introduces a new proof calculus for differential dynamic logic (dL) that is entirely based on uniform substitution, a proof rule that substitutes a formula for a predicate symbol everywhere. Uniform substitutions make it possible to rely on axioms rather than axiom schemata, substantially simplifying implementations. Instead of nontrivial schema variables and soundness-critical side con… ▽ More This paper introduces a new proof calculus for differential dynamic logic (dL) that is entirely based on uniform substitution, a proof rule that substitutes a formula for a predicate symbol everywhere. Uniform substitutions make it possible to rely on axioms rather than axiom schemata, substantially simplifying implementations. Instead of nontrivial schema variables and soundness-critical side conditions on the occurrence patterns of variables, the resulting calculus adopts only a finite number of ordinary dL formulas as axioms. The static semantics of differential dynamic logic is captured exclusively in uniform substitutions and bound variable renamings as opposed to being spread in delicate ways across the prover implementation. In addition to sound uniform substitutions, this paper introduces differential forms for differential dynamic logic that make it possible to internalize differential invariants, differential substitutions, and derivations as first-class axioms in dL. △ Less

Submitted 30 July, 2015; v1 submitted 6 March, 2015; originally announced March 2015.

MSC Class: 03F03; 03B70; 34A38 ACM Class: F.4.1; F.3.1; F.3.2; I.2.3

Differential Game Logic

Authors: André Platzer

Abstract: Differential game logic (dGL) is a logic for specifying and verifying properties of hybrid games, i.e. games that combine discrete, continuous, and adversarial dynamics. Unlike hybrid systems, hybrid games allow choices in the system dynamics to be resolved adversarially by different players with different objectives. The logic dGL can be used to study the existence of winning strategies for such… ▽ More Differential game logic (dGL) is a logic for specifying and verifying properties of hybrid games, i.e. games that combine discrete, continuous, and adversarial dynamics. Unlike hybrid systems, hybrid games allow choices in the system dynamics to be resolved adversarially by different players with different objectives. The logic dGL can be used to study the existence of winning strategies for such hybrid games, i.e. ways of resolving the player's choices in some way so that he wins by achieving his objective for all choices of the opponent. Hybrid games are determined, i.e. from each state, one player has a winning strategy, yet computing their winning regions may take transfinitely many steps. The logic dGL, nevertheless, has a sound and complete axiomatization relative to any expressive logic. Separating axioms are identified that distinguish hybrid games from hybrid systems. Finally, dGL is proved to be strictly more expressive than the corresponding logic of hybrid systems by characterizing the expressiveness of both. △ Less

Submitted 24 July, 2015; v1 submitted 8 August, 2014; originally announced August 2014.

Report number: CMU-CS-13-100R MSC Class: 03F03; 03B70; 34A38; 91A25 ACM Class: F.3.1, F.4.1

Journal ref: ACM Transactions on Computational Logic 17(1), pages 1:1-1:52, 2015

Collaborative Verification-Driven Engineering of Hybrid Systems

Authors: Stefan Mitsch, Grant Olney Passmore, Andre Platzer

Abstract: Hybrid systems with both discrete and continuous dynamics are an important model for real-world cyber-physical systems. The key challenge is to ensure their correct functioning w.r.t. safety requirements. Promising techniques to ensure safety seem to be model-driven engineering to develop hybrid systems in a well-defined and traceable manner, and formal verification to prove their correctness. The… ▽ More Hybrid systems with both discrete and continuous dynamics are an important model for real-world cyber-physical systems. The key challenge is to ensure their correct functioning w.r.t. safety requirements. Promising techniques to ensure safety seem to be model-driven engineering to develop hybrid systems in a well-defined and traceable manner, and formal verification to prove their correctness. Their combination forms the vision of verification-driven engineering. Often, hybrid systems are rather complex in that they require expertise from many domains (e.g., robotics, control systems, computer science, software engineering, and mechanical engineering). Moreover, despite the remarkable progress in automating formal verification of hybrid systems, the construction of proofs of complex systems often requires nontrivial human guidance, since hybrid systems verification tools solve undecidable problems. It is, thus, not uncommon for development and verification teams to consist of many players with diverse expertise. This paper introduces a verification-driven engineering toolset that extends our previous work on hybrid and arithmetic verification with tools for (i) graphical (UML) and textual modeling of hybrid systems, (ii) exchanging and comparing models and proofs, and (iii) managing verification tasks. This toolset makes it easier to tackle large-scale verification tasks. △ Less

Submitted 3 October, 2014; v1 submitted 24 March, 2014; originally announced March 2014.

MSC Class: 97M50 (Primary) 34K34; 68T15 (Secondary)

Journal ref: Math. Comput. Sci. 8(1), 71-97, 2014

A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems

Authors: Andre Platzer

Abstract: 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 may even form dynamic distributed networks, where neither structure nor dimension stay the same while the system follows hybrid dynamics, i.e., mixed discrete a… ▽ More 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 may even form dynamic distributed networks, where neither structure nor dimension stay the same while the system follows hybrid dynamics, i.e., mixed discrete and continuous dynamics. We provide the logical foundations for closing this analytic gap. We develop a formal model for distributed hybrid systems. It combines quantified differential equations with quantified assignments and dynamic dimensionality-changes. We introduce a dynamic logic for verifying distributed hybrid systems and present a proof calculus for this logic. This is the first formal verification approach for distributed hybrid systems. We prove that our calculus is a sound and complete axiomatization of the behavior of distributed hybrid systems relative to quantified differential equations. In our calculus we have proven collision freedom in distributed car control even when an unbounded number of new cars may appear dynamically on the road. △ Less

Submitted 22 November, 2012; v1 submitted 14 June, 2012; originally announced June 2012.

ACM Class: F.3.1, F.4.1, D.2.4, C.1.m, C.2.4, D.4.7

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 4 (November 26, 2012) lmcs:720

Dynamic Logics of Dynamical Systems

Authors: André Platzer

Abstract: 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 parametrized modal operators for each dynamical system to express necessary or possible properties of their transition behavior. Due to their full basis of first-order… ▽ More 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 parametrized modal operators for each dynamical system to express necessary or possible properties of their transition behavior. Due to their full basis of first-order modal logic operators, dynamic logics can express a rich variety of system properties, including safety, controllability, reactivity, liveness, and quantified parametrized properties, even about relations between multiple dynamical systems. In this survey, we focus on some of the representatives of the family of differential dynamic logics, which share the ability to express properties of dynamical systems having continuous dynamics described by various forms of differential equations. We explain the dynamical system models, dynamic logics of dynamical systems, their semantics, their axiomatizations, and proof calculi for proving logical formulas about these dynamical systems. We study differential invariants, i.e., induction principles for differential equations. We survey theoretical results, including soundness and completeness and deductive power. Differential dynamic logics have been implemented in automatic and interactive theorem provers and have been used successfully to verify safety-critical applications in automotive, aviation, railway, robotics, and analogue electrical circuits. △ Less

Submitted 21 May, 2012; originally announced May 2012.

Comments: Long version of LICS'12 invited tutorial DOI 10.1109/LICS.2012.13

MSC Class: 03B70; 03B45; 03F03; 68Q60; 34A38; 68M14; 34C45; 37H10; 60H10; 03D78 ACM Class: F.3.1; F.4.1; D.2.4; C.1.m; G.1.4; C.2.4; D.4.7; G.3

The Structure of Differential Invariants and Differential Cut Elimination

Authors: Andre Platzer

Abstract: The biggest challenge in hybrid systems verification is the handling of differential equations. Because computable closed-form solutions only exist for very simple differential equations, proof certificates have been proposed for more scalable verification. Search procedures for these proof certificates are still rather ad-hoc, though, because the problem structure is only understood poorly. We i… ▽ More The biggest challenge in hybrid systems verification is the handling of differential equations. Because computable closed-form solutions only exist for very simple differential equations, proof certificates have been proposed for more scalable verification. Search procedures for these proof certificates are still rather ad-hoc, though, because the problem structure is only understood poorly. We investigate differential invariants, which define an induction principle for differential equations and which can be checked for invariance along a differential equation just by using their differential structure, without having to solve them. We study the structural properties of differential invariants. To analyze trade-offs for proof search complexity, we identify more than a dozen relations between several classes of differential invariants and compare their deductive power. As our main results, we analyze the deductive power of differential cuts and the deductive power of differential invariants with auxiliary differential variables. We refute the differential cut elimination hypothesis and show that, unlike standard cuts, differential cuts are fundamental proof principles that strictly increase the deductive power. We also prove that the deductive power increases further when adding auxiliary differential variables to the dynamics. △ Less

Submitted 23 November, 2012; v1 submitted 11 April, 2011; originally announced April 2011.

ACM Class: math.CA

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 4 (November 21, 2012) lmcs:809