PTIME parametric verification of safety properties for reasonable linear hybrid automata

DOI10.1007/S11786-011-0098-XzbMath1262.68113OpenAlexW2121038072MaRDI QIDQ1949771

Werner Damm, Viorica Sofronie-Stokkermans, Carsten Ihlemann

Publication date: 16 May 2013

Published in: Mathematics in Computer Science (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/11858/00-001M-0000-0010-14F5-F

zbMATH Keywords

decidability and complexitylinear hybrid automataparametric verification of safety properties

Mathematics Subject Classification ID

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

Related Items (2)

Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata ⋮ PTIME parametric verification of safety properties for reasonable linear hybrid automata

Uses Software

• REDLOG
• z3
• LinAIG
• H-PILoT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
• Real addition and the polynomial hierarchy
• What's decidable about hybrid automata?
• Querying temporal and spatial constraint networks in PTIME
• PTIME parametric verification of safety properties for reasonable linear hybrid automata
• O-minimal hybrid systems.
• On the expressiveness and decidability of o-minimal hybrid systems
• GUARANTEED TERMINATION IN THE VERIFICATION OF LTL PROPERTIES OF NON-LINEAR ROBUST DISCRETE TIME HYBRID SYSTEMS
• Symbolic Reachability Analysis of Lazy Linear Hybrid Automata
• A Counterexample-Guided Approach to Parameter Synthesis for Linear Hybrid Automata
• Reasoning about temporal relations
• Algorithmic analysis of nonlinear hybrid systems
• Hybrid Systems: Computation and Control
• Automated Deduction – CADE-20
• Hybrid Systems: Computation and Control
• Hierarchical Reasoning for the Verification of Parametric Systems
• Tractable disjunctions of linear constraints: Basic results and applications to temporal reasoning

This page was built for publication: PTIME parametric verification of safety properties for reasonable linear hybrid automata