Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties

DOI10.1007/978-3-319-99154-2_8MaRDI QIDQ6104804zbMATH OpenOpenAlexFDO

Authors

Publication date 28 June 2023

Published in Quantitative Evaluation of Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1712.00275

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Abstract: Probabilistic timed automata (PTAs) are timed automata (TAs) extended with discrete probability distributions.They serve as a mathematical model for a wide range of applications that involve both stochastic and timed behaviours. In this work, we consider the problem of model-checking linear emph{dense-time} properties over {PTAs}. In particular, we study linear dense-time properties that can be encoded by TAs with infinite acceptance criterion.First, we show that the problem of model-checking PTAs against deterministic-TA specifications can be solved through a product construction. Based on the product construction, we prove that the computational complexity of the problem with deterministic-TA specifications is EXPTIME-complete. Then we show that when relaxed to general (nondeterministic) TAs, the model-checking problem becomes undecidable.Our results substantially extend state of the art with both the dense-time feature and the nondeterminism in TAs.

Recommendations

• scientific article; zbMATH DE number 1759607
• Model checking for probabilistic timed automata
• Probabilistic and Topological Semantics for Timed Automata
• Expressiveness and conciseness of timed automata for the verification of stochastic models
• Symbolic model checking for probabilistic timed automata
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Verifying automata specification of distributed probabilistic real-time systems
• Strict Divergence for Probabilistic Timed Automata
• Validation of Stochastic Systems

Cites work

• A theory of timed automata
• An extension of the inverse method to probabilistic timed automata
• Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata
• Automatic verification of real-time systems with discrete probability distributions.
• Concavely-Priced Probabilistic Timed Automata
• Efficient CTMC Model Checking of Linear Real-Time Objectives
• Fluid model checking of timed properties
• scientific article; zbMATH DE number 700091 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Measuring performance of continuous-time stochastic processes using timed automata
• Model checking for probabilistic timed automata
• Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
• Model Checking Probabilistic Timed Automata with One or Two Clocks
• On probabilistic timed automata.
• Performance analysis of probabilistic timed automata using digital clocks
• State explosion in almost-sure probabilistic reachability
• Stochastic games for verification of probabilistic timed automata
• Symbolic minimum expected time controller synthesis for probabilistic timed automata
• Symbolic model checking for probabilistic timed automata
• The benefits of relaxing punctuality
• Undecidability of Cost-Bounded Reachability in Priced Probabilistic Timed Automata

Cited in

(5)

• Consistency in parametric interval probabilistic timed automata
• Trace-Based Semantics for Probabilistic Timed I/O Automata
• Stochastic games for verification of probabilistic timed automata
• Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties
• Expressiveness and conciseness of timed automata for the verification of stochastic models

This page was built for publication: Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties

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