Consistency in parametric interval probabilistic timed automata

DOI10.1016/J.JLAMP.2019.04.007MaRDI QIDQ2291816zbMATH OpenOpenAlexWikidataFDO

Authors Étienne André, Paulin Fournier, Benoît Delahaye

Publication date 31 January 2020

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

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

zbMATH Keywords

parametric probabilistic timed automataparametric verificationtimed probabilistic systems

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: We propose a new abstract formalism for probabilistic timed systems, Parametric Interval Probabilistic Timed Automata, based on an extension of Parametric Timed Automata and Interval Markov Chains. In this context, we consider the consistency problem that amounts to deciding whether a given specification admits at least one implementation. In the context of Interval Probabilistic Timed Automata (with no timing parameters), we show that this problem is decidable and propose a constructive algorithm for its resolution. We show that the existence of timing parameter valuations ensuring consistency is undecidable in the general context, but still exhibit a syntactic condition on parameters to ensure decidability. We also propose procedures that resolve both the consistency and the consistent reachability problems when the parametric probabilistic zone graph is finite.

Recommendations

• Verifying quantitative properties of continuous probabilistic timed automata
• Probabilistic and Topological Semantics for Timed Automata
• Model checking for probabilistic timed automata
• On the expressiveness of parametric timed automata
• A TIMED FAILURE EQUIVALENCE PRESERVING ABSTRACTION FOR PARAMETRIC TIME-INTERVAL AUTOMATA
• Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties
• Robust parametric reachability for timed automata
• Concavely-Priced Probabilistic Timed Automata

Cites work

• A theory of timed automata
• Abstract probabilistic automata
• An extension of the inverse method to probabilistic timed automata
• AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA
• Automatic verification of real-time systems with discrete probability distributions.
• Consistency and refinement for interval Markov chains
• Consistency for parametric interval Markov chains
• Decidability and complexity results for timed automata and semi-linear hybrid automta
• Decision problems for lower/upper bound parametric timed automata
• Language emptiness of continuous-time parametric timed automata
• Language preservation problems in parametric timed automata
• Lectures on Concurrency and Petri Nets
• Linear parametric model checking of timed automata
• Parameter synthesis for parametric interval Markov chains
• Parameter synthesis for probabilistic timed automata using stochastic game abstractions
• Parametric real-time reasoning
• Performance analysis of probabilistic timed automata using digital clocks
• Probabilistic model checking of deadline properties in the IEEE 1394 fireWire root contention protocol
• Robust parametric reachability for timed automata

Cited in

(1)

• Tweaking the odds in probabilistic timed automata

This page was built for publication: Consistency in parametric interval probabilistic timed automata

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