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

DOI10.1007/978-3-319-24246-0_12MaRDI QIDQ2964462zbMATH OpenOpenAlexFDO

Authors Werner Damm, Matthias Horbach, Viorica Sofronie-Stokkermans

Publication date 27 February 2017

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

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

Mathematics Subject Classification ID

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

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.

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

Cites work

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

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

Describes a project that uses

Uses Software

• H-PILoT
• z3

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)