Efficient model-checking of dense-time systems with time-convexity analysis

DOI10.1016/J.TCS.2012.09.019MaRDI QIDQ1935781zbMATH OpenOpenAlexFDO

Authors Farn Wang

Publication date 19 February 2013

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2012.09.019

zbMATH Keywords

verificationconvexmodel-checkingtimed automatonTCTLtime convextimed inevitabilitytimed precondition

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions
• Model-checking in dense real-time
• Model-checking dense-time duration calculus
• The automatic verification using symbolic model-checking
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems

Cited in

(6)

• TCTL inevitability analysis of dense-time systems
• Convex Programs for Temporal Verification of Nonlinear Dynamical Systems
• Model Checking Real-Time Systems
• Optimal time-bounded reachability analysis for concurrent systems
• Efficient timed model checking for discrete-time systems
• Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions

Describes a project that uses

Uses Software

• Kronos

This page was built for publication: Efficient model-checking of dense-time systems with time-convexity analysis

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