Statistical Model Checking for Networks of Priced Timed Automata

DOI10.1007/978-3-642-24310-3_7MaRDI QIDQ3172845zbMATH OpenOpenAlexFDO

Authors Alexandre David, Axel Legay, Marius Mikučionis, Danny Bøgsted Poulsen, Jonas van Vliet, Zheng Wang, Kim G. Larsen

Publication date 7 October 2011

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-24310-3_7

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Recommendations

• scientific article; zbMATH DE number 7333236
• Statistical probabilistic model checking with a focus on time-bounded properties
• Validation of Stochastic Systems
• Parameterized model checking of networks of timed automata with Boolean guards
• Symbolic model checking for probabilistic timed automata

Cites work

• A compositional translation of timed automata with deadlines to Uppaal timed automata
• A theory of timed automata
• Bayesian statistical model checking with application to Simulink/Stateflow verification
• Bisimulation through probabilistic testing
• Computer Aided Verification
• Computer Aided Verification
• Constraint-based analysis of concurrent probabilistic hybrid systems: an application to networked automation systems
• Formal Methods for the Design of Real-Time Systems
• scientific article; zbMATH DE number 1361136 (Why is no real title available?)
• scientific article; zbMATH DE number 1794360 (Why is no real title available?)
• scientific article; zbMATH DE number 1794367 (Why is no real title available?)
• scientific article; zbMATH DE number 1905115 (Why is no real title available?)
• scientific article; zbMATH DE number 3045589 (Why is no real title available?)
• Hybrid systems: computation and control. 4th international workshop, HSCC 2001, Rome, Italy, March 28--30, 2001. Proceedings
• Labelled Markov processes.
• Probabilistic and Topological Semantics for Timed Automata
• The algorithmic analysis of hybrid systems
• Timed I/O automata: a complete specification theory for real-time systems
• Verification, Model Checking, and Abstract Interpretation

Cited in

(9)

• A maximal entropy stochastic process for a timed automaton
• Monitor-based statistical model checking for weighted metric temporal logic
• Model-based verification, optimization, synthesis and performance evaluation of real-time systems
• Robust synthesis for real-time systems
• Integrating deployment architectures and resource consumption in timed object-oriented models
• Applications of an expressive statistical model checking approach to the analysis of genetic circuits
• Parametric analyses of attack-fault trees
• scientific article; zbMATH DE number 7333236 (Why is no real title available?)
• Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signals

Describes a project that uses

Uses Software

• PHAVer
• Uppaal
• HyTech
• Ymer
• APMC

This page was built for publication: Statistical Model Checking for Networks of Priced Timed Automata

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