KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)

2008 ◽  
pp. 171-178 ◽  
Author(s):  
André Platzer ◽  
Jan-David Quesel
Keyword(s):  
Hybrid Systems ◽  
Theorem Prover ◽  
System Description

scholarly journals The Lean Theorem Prover (System Description)

2015 ◽  
pp. 378-388 ◽  
Author(s):  
Leonardo de Moura ◽  
Soonho Kong ◽  
Jeremy Avigad ◽  
Floris van Doorn ◽  
Jakob von Raumer
Keyword(s):  
Theorem Prover ◽  
System Description

scholarly journals Model-Based Diagnosis of Hybrid Systems Using Satisfiability Modulo Theory

2019 ◽  
Vol 33 ◽  
pp. 1452-1459 ◽  
Author(s):  
Alexander Diedrich ◽  
Alexander Maier ◽  
Oliver Niggemann
Keyword(s):  
State Space ◽  
Hybrid Systems ◽  
State Space Models ◽  
Satisfiability Modulo Theory ◽  
Tank Model ◽  
Tennessee Eastman Process ◽  
Minimum Cardinality ◽  
System Description ◽  
Model Based ◽  
Human Operators

Currently, detecting and isolating faults in hybrid systems is often done manually with the help of human operators. In this paper we present a novel model-based diagnosis approach for automatically diagnosing hybrid systems. The approach has two parts: First, modelling dynamic system behaviour is done through well-known state space models using differential equations. Second, from the state space models we calculate Boolean residuals through an observer-pattern. The novelty lies in implementing the observer pattern through the use of a symbolic system description specified in satisfiability theory modulo linear arithmetic. With this, we create a static situation for the diagnosis algorithm and decouple modelling and diagnosis. Evaluating the system description generates one Boolean residual for each component. These residuals constitute the fault symptoms. To find the minimum cardinality diagnosis from these symptoms we employ Reiter’s diagnosis lattice.For the experimental evaluation we use a simulation of the Tennessee Eastman process and a simulation of a four-tank model. We show that the presented approach is able to identify all injected faults.

scholarly journals Real Analysis for Complex Systems

10.29007/ksvj ◽  
2018 ◽  
Author(s):  
Andrè Platzer
Keyword(s):  
Differential Equations ◽  
Hybrid Systems ◽  
Traffic Control ◽  
Theoretical Perspective ◽  
Practical Interest ◽  
Theorem Prover ◽  
Physical Systems ◽  
Systems Model ◽  
Model Complex ◽  
Verification Techniques

Formal verification techniques are used routinely in finite-state digital circuits. Theorem proving is also used successfully for infinite-state discrete systems. But many safety-critical computers are actually embedded in physical systems. Hybrid systems model complex physical systems as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. They arise frequently in many application domains, including aviation, automotive, railway, and robotics. There is a well-understood theory for proving programs. But what about complex physical systems? How can we prove that a hybrid system works as expected, e.g., an aircraft does not crash into another one?This talk illustrates the complexities and pitfalls of hybrid systems verification. It describes a theoretical and practical foundation for deductive verification of hybrid systems called differential dynamic logic. The proof calculus for this logic is interesting from a theoretical perspective, because it is a complete axiomatization of hybrid systems relative to differential equations. The approach is of considerable practical interest too. Its implementation in the theorem prover KeYmaera has been used successfully to verify collision avoidance properties in the European Train Control System and air traffic control systems. The number of dimensions and nonlinearities in they hybrid dynamics of these systems is surprisingly tricky such that they are still out of scope for other verification tools.

scholarly journals Leo-III Version 1.1 (System description)

10.29007/grmx ◽  
2018 ◽  
Author(s):  
Christoph Benzmüller ◽  
Alexander Steen ◽  
Max Wisniewski
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
Theorem Prover ◽  
Higher Order Logic ◽  
System Description ◽  
Agent Based ◽  
First Order ◽  
Theorem Provers ◽  
Automated Theorem Prover ◽  
Ordering Constraints

Leo-III is an automated theorem prover for (polymorphic) higher-order logic which supports all common TPTP dialects, including THF, TFF and FOF as well as their rank-1 polymorphic derivatives. It is based on a paramodulation calculus with ordering constraints and, in tradition of its predecessor LEO-II, heavily relies on cooperation with external first-order theorem provers.Unlike LEO-II, asynchronous cooperation with typed first-order provers and an agent-based internal cooperation scheme is supported. In this paper, we sketch Leo-III's underlying calculus, survey implementation details and give examples of use.

scholarly journals Automated Reasoning in the Simulation of Evolvable Systems

10.29007/jj86 ◽  
2018 ◽  
Author(s):  
Djihed Afifi ◽  
David Rydeheard ◽  
Howard Barringer
Keyword(s):  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Rapid Assessment ◽  
Theorem Prover ◽  
System Description ◽  
Large Sets ◽  
Simulation Engine ◽  
Meta Level ◽  
Almost All ◽  
Computational Systems

We present a novel application of automated theorem proving for the simulation of computational systems. The computational systems we consider are evolvable, i.e. may reconfigure their structure and programs at run-time. In [1], a logical framework for describing such systems is introduced. The underlying logic of this framework allows us to build a simulation engine for executing system specifications. This engine makes intensive use of automated theorem proving – when running a simulation, almost all computational steps are those of a theorem prover. In this paper, we present this novel combination of a logical setting involving meta-level logics and large sets of formulae for system description, together with theorem proving requirements which involve often slowly changing specifications with the need for rapid assessment of deducibility and consistency. We will evaluate the suitability of several theorem provers for this application.

Sign in / Sign up

Export Citation Format

Share Document