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

DOI10.1016/J.TCS.2012.09.019zbMATH Open1279.68222OpenAlexW2098021313MaRDI QIDQ1935781FDOQ1935781

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

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

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)

Cited In (6)

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

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)