Model measuring for discrete and hybrid systems

DOI10.1016/j.nahs.2016.09.001zbMath1401.68198OpenAlexW2529208763MaRDI QIDQ2374564

Jan Otop, Thomas A. Henzinger

Publication date: 15 December 2016

Published in: Nonlinear Analysis. Hybrid Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.nahs.2016.09.001

zbMATH Keywords

weighted automataquantitative model checkingmodel measuringparametric hybrid automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Related Items (3)

Unnamed Item ⋮ Non-deterministic Weighted Automata on Random Words ⋮ Non-deterministic weighted automata evaluated over Markov chains

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A survey of timed automata for the development of real-time systems
• \(E\)-unification with constants vs. general \(E\)-unification
• Robust reachability in timed automata and games: a game-based approach
• Optimal paths in weighted timed automata
• The algorithmic analysis of hybrid systems
• Robustness of temporal logic specifications for continuous-time signals
• Simulation distances
• Handbook of weighted automata
• Robust safety of timed automata
• Enhancing model checking in verification by AI techniques
• Linear parametric model checking of timed automata
• On the optimal reachability problem of weighted timed automata
• Lipschitz Robustness of Timed I/O Systems
• PARAMETRIC VERIFICATION AND TEST COVERAGE FOR HYBRID AUTOMATA USING THE INVERSE METHOD
• From Model Checking to Model Measuring
• Model measuring for hybrid systems
• On Reachability for Hybrid Automata over Bounded Time
• Robust Model-Checking of Timed Automata via Pumping in Channel Machines
• A Counterexample-Guided Approach to Parameter Synthesis for Linear Hybrid Automata
• Quantitative Languages
• Concavely-Priced Timed Automata
• Robust Satisfaction of Temporal Logic over Real-Valued Signals
• Stability radii of linear discrete‐time systems and symplectic pencils
• Discount-Optimal Infinite Runs in Priced Timed Automata
• An automata-theoretic approach to branching-time model checking
• Formal Methods for the Design of Real-Time Systems

This page was built for publication: Model measuring for discrete and hybrid systems