Hypervolume Approximation in Timed Automata Model Checking

DOI10.1007/978-3-540-75454-1_7MaRDI QIDQ3510836zbMATH OpenOpenAlexFDO

Authors V. Braberman, Jorge Lucángeli Obes, A. Olivero, F. Schapachnik

Publication date 3 July 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-75454-1_7

Mathematics Subject Classification ID

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

Recommendations

• Bounded model checking for timed automata
• Verified model checking of timed automata
• Bounded Model Checking for Parametric Timed Automata
• On reachability for hybrid automata over bounded time
• Template-based unbounded time verification of affine hybrid automata
• Using non-convex approximations for efficient analysis of timed automata
• scientific article; zbMATH DE number 5024617
• Verification of timed automata via satisfiability checking
• Durations and parametric model-checking in timed automata
• scientific article; zbMATH DE number 1444359

Cited in

(4)

• A quadratic-time DBM-based successor algorithm for checking timed automata
• Entropy of regular timed languages
• Model Checking Timed Automata with Priorities Using DBM Subtraction
• Improving the construction of the DBM over-approximation of the state space of real-time preemptive systems

Describes a project that uses

Uses Software

• Kronos
• Uppaal

This page was built for publication: Hypervolume Approximation in Timed Automata Model Checking

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