Parametric real-time reasoning

DOI10.1145/167088.167242zbMath1310.68139OpenAlexW2025782239MaRDI QIDQ5248530

Moshe Y. Vardi, Rajeev Alur, Thomas A. Henzinger

Publication date: 7 May 2015

Published in: Proceedings of the twenty-fifth annual ACM symposium on Theory of computing - STOC '93 (Search for Journal in Brave)

Full work available at URL: https://hdl.handle.net/1813/6111

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (74)

Stubborn set reduction for timed reachability and safety games ⋮ Tweaking the odds in probabilistic timed automata ⋮ \textsf{IMITATOR} 3: synthesis of timing parameters beyond decidability ⋮ Updatable timed automata ⋮ Efficient scaling-invariant checking of timed bisimulation ⋮ Parameter Synthesis for Probabilistic Timed Automata Using Stochastic Game Abstractions ⋮ Language Emptiness of Continuous-Time Parametric Timed Automata ⋮ Model Checking Real-Time Systems ⋮ Verification of Hybrid 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 ⋮ Reachability in Succinct and Parametric One-Counter Automata ⋮ On clock-aware LTL parameter synthesis of timed automata ⋮ Unnamed Item ⋮ LTL Parameter Synthesis of Parametric Timed Automata ⋮ Parametric probabilistic transition systems for system design and analysis ⋮ Shrinking of time Petri nets ⋮ Discrete Parameters in Petri Nets ⋮ Robust synthesis for real-time systems ⋮ Language Preservation Problems in Parametric Timed Automata ⋮ Parameterized Weighted Containment ⋮ A survey of timed automata for the development of real-time systems ⋮ Unnamed Item ⋮ Quantitative analysis of interval Markov chains ⋮ Distributed parametric model checking timed automata under non-zenoness assumption ⋮ Generalized discrete timed automata: Decidable approximations for safety verification. ⋮ Parameter Synthesis for Bounded Cost Reachability in Time Petri Nets ⋮ Low dimensional hybrid systems -- decidable, undecidable, don't know ⋮ Parametric updates in parametric timed automata ⋮ Coefficient synthesis for threshold automata ⋮ Pattern Matching and Parameter Identification for Parametric Timed Regular Expressions ⋮ Parametric Verification of Weighted Systems ⋮ Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph ⋮ New decidability results concerning two-way counter machines and applications ⋮ Robust reachability in timed automata and games: a game-based approach ⋮ Parametric Timed Model Checking for Guaranteeing Timed Opacity ⋮ Parametric metric interval temporal logic ⋮ Parameter synthesis for hierarchical concurrent real-time systems ⋮ An algorithm for single-source shortest paths enumeration in parameterized weighted graphs ⋮ Interval logics and their decision procedures. II: A real-time interval logic ⋮ On completeness of liveness synthesis for parametric timed automata (Extended Abstract) ⋮ On parametric timed automata and one-counter machines ⋮ The language preservation problem is undecidable for parametric event-recording automata ⋮ An extension of the inverse method to probabilistic timed automata ⋮ Formal verification of multitasking applications based on timed automata model ⋮ Specification Theories for Probabilistic and Real-Time Systems ⋮ A menagerie of timed automata ⋮ Reachability solution characterization of parametric real-time systems ⋮ A real-time interval logic and its decision procedure ⋮ Unnamed Item ⋮ What’s Decidable About Parametric Timed Automata? ⋮ Reachability in parametric interval Markov chains using constraints ⋮ Time-budgeting: a component based development methodology for real-time embedded systems ⋮ Consistency in parametric interval probabilistic timed automata ⋮ Iterative bounded synthesis for efficient cycle detection in parametric timed automata ⋮ Unnamed Item ⋮ On minimal elements of upward-closed sets ⋮ What's decidable about hybrid automata? ⋮ An Inverse Method for Parametric Timed Automata ⋮ Formalized Timed Automata ⋮ A game approach to the parametric control of real-time systems ⋮ Decision problems for lower/upper bound parametric timed automata ⋮ The Complexity of Flat Freeze LTL ⋮ Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques ⋮ Time Unbalanced Partial Order ⋮ Linear parametric model checking of timed automata ⋮ Zone-based verification of timed automata: extrapolations, simulations and what next? ⋮ Efficient convex zone merging in parametric timed automata ⋮ Parametric Schedulability Analysis of a Launcher Flight Control System under Reactivity Constraints* ⋮ Parametric Analyses of Attack-fault Trees* ⋮ Cost Problems for Parametric Time Petri Nets* ⋮ Continuous One-counter Automata

This page was built for publication: Parametric real-time reasoning