Model checking for a class of weighted automata
From MaRDI portal
Abstract: A large number of different model checking approaches has been proposed during the last decade. The different approaches are applicable to different model types including untimed, timed, probabilistic and stochastic models. This paper presents a new framework for model checking techniques which includes some of the known approaches, but enlarges the class of models for which model checking can be applied to the general class of weighted automata. The approach allows an easy adaption of model checking to models which have not been considered yet for this purpose. Examples for those new model types for which model checking can be applied are max/plus or min/plus automata which are well established models to describe different forms of dynamic systems and optimization problems. In this context, model checking can be used to verify temporal or quantitative properties of a system. The paper first presents briefly our class of weighted automata, as a very general model type. Then Valued Computational Tree Logic (CTL formula are presented. As a last result, a bisimulation is presented for weighted automata and for CTL$.
Recommendations
Cites work
- A Compositional Approach to Performance Modelling
- A logic for reasoning about time and reliability
- A theory of timed automata
- Algebraic laws for nondeterminism and concurrency
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Bisimulation relations for weighted automata
- Bisimulation through probabilistic testing
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- scientific article; zbMATH DE number 1696660 (Why is no real title available?)
- scientific article; zbMATH DE number 3932372 (Why is no real title available?)
- scientific article; zbMATH DE number 3716792 (Why is no real title available?)
- scientific article; zbMATH DE number 42752 (Why is no real title available?)
- scientific article; zbMATH DE number 3511563 (Why is no real title available?)
- scientific article; zbMATH DE number 627763 (Why is no real title available?)
- scientific article; zbMATH DE number 2040321 (Why is no real title available?)
- scientific article; zbMATH DE number 1358710 (Why is no real title available?)
- scientific article; zbMATH DE number 1884420 (Why is no real title available?)
- scientific article; zbMATH DE number 1916666 (Why is no real title available?)
- scientific article; zbMATH DE number 1445805 (Why is no real title available?)
- Min-max Computation Tree Logic
- Model-checking in dense real-time
- Performance evaluation of (max,+) automata
- Polytime model checking for times probabilistic computation tree logic
- Reduced systems in Markov chains and their applications in queueing theory
- Symbolic model checking: \(10^{20}\) states and beyond
- Weighted timed automata: model-checking and games
Cited in
(8)- Model checking and synthesis for branching multi-weighted logics
- Adding pebbles to weighted automata: easy specification \& efficient evaluation
- Parameterized model checking of weighted networks
- Monitor-based statistical model checking for weighted metric temporal logic
- A new model for model checking: cycle-weighted Kripke structure
- Parametric verification of weighted systems
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- Model checking computation tree logic over finite lattices
This page was built for publication: Model checking for a class of weighted automata
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5962025)
