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

lmcs:720 - Logical Methods in Computer Science, November 26, 2012, Volume 8, Issue 4 -
A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems

Authors: Andre Platzer ORCID-iD

    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.

    Volume: Volume 8, Issue 4
    Published on: November 26, 2012
    Accepted on: June 25, 2015
    Submitted on: January 7, 2011
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,Mathematics - Dynamical Systems,F.3.1, F.4.1, D.2.4, C.1.m, C.2.4, D.4.7
    Fundings :
      Source : OpenAIRE Research Graph
    • CPS: Medium: GOALI: An Architecture Approach to Heterogeneous Verfication of Cyber-Physical Systems; Funder: National Science Foundation; Code: 1035800
    • Collaborative Research: Next-Generation Model Checking and Abstract Interpretation with a Focus on Embedded Control and Systems Biology; Funder: National Science Foundation; Code: 0926181
    • CAREER: Logical Foundations of Cyber-Physical Systems; Funder: National Science Foundation; Code: 1054246
    • CPS: Small: Compositionality and Reconfiguration for Distributed Hybrid Systems; Funder: National Science Foundation; Code: 0931985

    Linked data

    Source : ScholeXplorer IsReferencedBy ARXIV 1408.1980
    Source : ScholeXplorer IsReferencedBy DOI 10.1145/2817824
    Source : ScholeXplorer IsReferencedBy DOI 10.1184/r1/6604844
    Source : ScholeXplorer IsReferencedBy DOI 10.1184/r1/6604844.v1
    Source : ScholeXplorer IsReferencedBy DOI 10.48550/arxiv.1408.1980
    • 10.1184/r1/6604844
    • 10.48550/arxiv.1408.1980
    • 10.1145/2817824
    • 10.1145/2817824
    • 10.1145/2817824
    • 1408.1980
    • 10.1184/r1/6604844.v1
    Differential Game Logic
    Platzer, Andre ;

    16 Documents citing this article


    Consultation statistics

    This page has been seen 831 times.
    This article's PDF has been downloaded 403 times.