Decidability of verification of safety properties of spatial families of linear hybrid automata

DOI10.1007/978-3-319-24246-0_12zbMATH Open1471.68114arXiv1601.01648OpenAlexW2230509950MaRDI QIDQ2964462FDOQ2964462

Authors: Werner Damm, Matthias Horbach, Viorica Sofronie-Stokkermans 

Publication date: 27 February 2017

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Abstract: We consider systems composed of an unbounded number of uniformly designed linear hybrid automata, whose dynamic behavior is determined by their relation to neighboring systems. We present a class of such systems and a class of safety properties whose verification can be reduced to the verification of (small) families of neighbouring systems of bounded size, and identify situations in which such verification problems are decidable, resp. fixed parameter tractable. We illustrate the approach with an example from coordinated vehicle guidance, and describe an implementation which allows us to perform such verification tasks automatically.

Full work available at URL: https://arxiv.org/abs/1601.01648

Recommendations

• Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata
• Safety verification of non-linear hybrid systems is quasi-decidable
• Safety verification of non-linear hybrid systems is quasi-semidecidable
• PTIME parametric verification of safety properties for reasonable linear hybrid automata
• Uniformity for the decidability of hybrid automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Differential dynamic logic for hybrid systems
• All for the price of few (parameterized verification through view abstraction)
• Reasoning about temporal relations
• Towards Complete Reasoning about Axiomatic Specifications
• On Local Reasoning in Verification
• Computer Aided Verification
• Real addition and the polynomial hierarchy
• Automated Deduction – CADE-20
• A Counterexample-Guided Approach to Parameter Synthesis for Linear Hybrid Automata
• Tractable disjunctions of linear constraints: Basic results and applications to temporal reasoning
• Quantified Differential Dynamic Logic for Distributed Hybrid Systems
• On Hierarchical Reasoning in Combinations of Theories
• Parameterized Synthesis
• Hierarchical reasoning for the verification of parametric systems
• PTIME parametric verification of safety properties for reasonable linear hybrid automata
• Hierarchical reasoning and model generation for the verification of parametric hybrid systems
• Parametric verification and test coverage for hybrid automata using the inverse method
• Can we build it: formal synthesis of control strategies for cooperative driver assistance systems
• Decidability of verification of safety properties of spatial families of linear hybrid automata

Cited In (5)

• Safety verification of trajectory planning for multiple robots
• Verification of cooperating traffic agents
• Decidability of verification of safety properties of spatial families of linear hybrid automata
• Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata
• Formal Methods for Components and Objects

Uses Software

• z3
• H-PILoT

This page was built for publication: Decidability of verification of safety properties of spatial families of linear hybrid automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2964462)