Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions

DOI10.1007/978-3-540-88387-6_24MaRDI QIDQ3540075zbMATH OpenOpenAlexFDO

Authors Farn Wang

Publication date 20 November 2008

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-88387-6_24

zbMATH Keywords

concaveconvexmodel-checkingTCTLtime progresstimed automaton

Mathematics Subject Classification ID

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

Recommendations

• Efficient model-checking of dense-time systems with time-convexity analysis
• Model-checking in dense real-time
• scientific article; zbMATH DE number 2080039
• TCTL inevitability analysis of dense-time systems
• Symbolic Simulation-Checking of Dense-Time Automata

Cites work

• A theory of timed automata
• scientific article; zbMATH DE number 176728 (Why is no real title available?)
• Kronos: A verification tool for real-time systems
• Symbolic model checking for real-time systems

Cited in

(4)

• Efficient model-checking of dense-time systems with time-convexity analysis
• A menagerie of timed automata
• scientific article; zbMATH DE number 5201490 (Why is no real title available?)
• HRELTL: a temporal logic for hybrid systems

Describes a project that uses

Uses Software

• Kronos
• Uppaal

This page was built for publication: Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions

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