Linear parametric model checking of timed automata
From MaRDI portal
Publication:1858447
DOI10.1016/S1567-8326(02)00037-1zbMath1008.68069OpenAlexW2155953212MaRDI QIDQ1858447
Thomas Hune, Judi Romijn, Mariëlle I. A. Stoelinga, Frits W. Vaandrager
Publication date: 13 February 2003
Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s1567-8326(02)00037-1
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (37)
Tweaking the odds in probabilistic timed automata ⋮ Parameter Synthesis for Probabilistic Timed Automata Using Stochastic Game Abstractions ⋮ Model measuring for discrete and hybrid systems ⋮ Model Checking Real-Time Systems ⋮ Robust parametric reachability for timed automata ⋮ Parametric Deadlock-Freeness Checking Timed Automata ⋮ Parameter synthesis for probabilistic timed automata using stochastic game abstractions ⋮ Unnamed Item ⋮ On clock-aware LTL parameter synthesis of timed automata ⋮ Analysis of a biphase mark protocol with Uppaal and PVS ⋮ LTL Parameter Synthesis of Parametric Timed Automata ⋮ Robust synthesis for real-time systems ⋮ Language Preservation Problems in Parametric Timed Automata ⋮ Unnamed Item ⋮ Distributed parametric model checking timed automata under non-zenoness assumption ⋮ Parameter Synthesis for Bounded Cost Reachability in Time Petri Nets ⋮ Parametric updates in parametric timed automata ⋮ Parametric Verification of Weighted Systems ⋮ Parametric Timed Model Checking for Guaranteeing Timed Opacity ⋮ Parametric metric interval temporal logic ⋮ Parameter synthesis for hierarchical concurrent real-time systems ⋮ On completeness of liveness synthesis for parametric timed automata (Extended Abstract) ⋮ Automatic generation of path conditions for concurrent timed systems ⋮ An extension of the inverse method to probabilistic timed automata ⋮ Hierarchical Reasoning for the Verification of Parametric Systems ⋮ Unnamed Item ⋮ What’s Decidable About Parametric Timed Automata? ⋮ Consistency in parametric interval probabilistic timed automata ⋮ Iterative bounded synthesis for efficient cycle detection in parametric timed automata ⋮ A game approach to the parametric control of real-time systems ⋮ Time based deadlock prevention for Petri nets ⋮ Decision problems for lower/upper bound parametric timed automata ⋮ Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques ⋮ Time Unbalanced Partial Order ⋮ Efficient convex zone merging in parametric timed automata ⋮ Parametric Schedulability Analysis of a Launcher Flight Control System under Reactivity Constraints* ⋮ Cost Problems for Parametric Time Petri Nets*
Uses Software
Cites Work
- A theory of timed automata
- Fun with fireWire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol
- Uppaal in a nutshell
- Parametric real-time reasoning
- Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Linear parametric model checking of timed automata