Platzer, André (2008) Differential dynamic logics - automated theorem proving for hybrid systems. PhD, Universität Oldenburg.

Preview

Volltext (1916Kb)

Abstract

Hybrid systems are models for complex physical systems and are defined as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. With the goal of developing a theoretical and practical foundation for deductive verification of hybrid systems, we introduce differential dynamic logic as a new logic with which correctness properties of hybrid systems with parameterized system dynamics can be specified and verified naturally. As a verification technique that is suitable for automation, we introduce a free variable proof calculus with a novel combination of real-valued free variables and Skolemisation for lifting quantifier elimination for real arithmetic to dynamic logic. The calculus is compositional, i.e., it reduces properties of hybrid systems successively to properties of their parts. Our main result proves that this calculus axiomatises the transition behaviour of hybrid systems completely relative to differential equations.

["eprint_fieldname_abstract_plus" not defined]

Hybride Systeme sind Modelle für komplexe physikalische Systeme und als dynamische Systeme mit interagierenden diskreten Transitionen und kontinuierlichen Evolutionen längs Differentialgleichungen definiert. Mit dem Ziel, ein theoretisches und praktisches Fundament für die deduktive Verifikation hybrider Systeme zu entwickeln, stellen wir differentielle dynamische Logik als eine neue Logik vor, mit der Korrektheitsaussagen von hybriden Systemen mit parametrischer Systemdynamik auf natürliche Art und Weise spezifiziert und verifiziert werden können. Als Verifikationstechnik die sich zur Automatisierung eignet führen wir ferner einen Beweiskalkül ein, der eine neuartige Kombination reell-wertiger freier Variablen mit Skolemisierung besitzt, um Quantorenelimination für reelle Arithmetik auf dynamische Logik zu liften. Der Kalkül arbeitet kompositionell, d.h., er reduziert Eigenschaften von hybriden Systemen sukzessive auf Eigenschaften ihrer Bestandteile. Unser Hauptresultat zeigt, dass dieser Kalkül das Transitionsverhalten hybrider Systeme vollständig relativ zu Differentialgleichungen axiomatisiert.

Item Type:	Thesis (PhD)
Uncontrolled Keywords:	dynamische Logik , Differentialgleichung , hybrides System , Axiomatisierung
Controlled Keywords:	Informatik
Subjects:	Generalities, computers, information > Computer science, internet
Divisions:	School of Computing Science, Business Administration, Economics and Law School of Computing Science, Business Administration, Economics and Law > Department of Computing Science
Date Deposited:	17 Jan 2013 14:29
Last Modified:	08 Jul 2013 13:04
URI:	https://oops.uni-oldenburg.de/id/eprint/1403
URN:	urn:nbn:de:gbv:715-oops-14833
DOI:
Nutzungslizenz:

Actions (login required)

View Item