Reachability and liveness in parametric timed automata

MaRDI QIDQ5094115zbMATH OpenFDO

Authors Étienne André, Didier Lime, Olivier H. Roux

Publication date 2 August 2022

Full work available at URL https://arxiv.org/abs/2004.09171, https://lmcs.episciences.org/9070

zbMATH Keywords

deadlock-freenessL/U-PTAlivenessparametric timed automatareachability

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• TCTL model checking lower/upper-bound parametric timed automata without invariants
• What's decidable about parametric timed automata?
• Decision Problems for Lower/Upper Bound Parametric Timed Automata
• Decision problems for lower/upper bound parametric timed automata
• Robust parametric reachability for timed automata

Cites work

• A theory of timed automata
• Advances in Parametric Real-Time Reasoning
• AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA
• Analysis of timed systems using time-abstracting bisimulations
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Decision problems for lower/upper bound parametric timed automata
• Durations and parametric model-checking in timed automata
• scientific article; zbMATH DE number 4089320 (Why is no real title available?)
• scientific article; zbMATH DE number 1759608 (Why is no real title available?)
• scientific article; zbMATH DE number 1444359 (Why is no real title available?)
• scientific article; zbMATH DE number 3310089 (Why is no real title available?)
• Integer-complete synthesis for bounded parametric timed automata
• Language preservation problems in parametric timed automata
• Lectures on Concurrency and Petri Nets
• Linear parametric model checking of timed automata
• MTL-model checking of one-clock parametric timed automata is undecidable
• On parametric timed automata and one-counter machines
• On the expressiveness of parametric timed automata
• Parametric model-checking of stopwatch Petri nets
• Parametric real-time reasoning
• Parametric timing analysis for real-time systems
• Parametric updates in parametric timed automata
• Proving the Correctness of Multiprocess Programs
• Real-Time Model-Checking: Parameters everywhere
• Robust parametric reachability for timed automata
• TCTL model checking lower/upper-bound parametric timed automata without invariants
• Untimed Language Preservation in Timed Systems
• What's decidable about hybrid automata?

Cited in

(8)

• Presburger liveness verification of discrete timed automata.
• Effective definability of the reachability relation in timed automata
• Parametric Deadlock-Freeness Checking Timed Automata
• scientific article; zbMATH DE number 1538037 (Why is no real title available?)
• Parametric updates in parametric timed automata
• scientific article; zbMATH DE number 7297846 (Why is no real title available?)
• Parametric updates in parametric timed automata
• Dense integer-complete synthesis for bounded parametric timed automata

This page was built for publication: Reachability and liveness in parametric timed automata

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