An Experiment on Decision Diagrams for Model Checking Probabilistic Timed Automata
1
Citation
37
Reference
10
Related Paper
Citation Trend
Abstract:
The state-of-the-art model-checkers for probabilistic timed automata (PTAs) use separate representations for the dense-time and discrete parts of PTA states. In the literature, integrated state-space representations based on decision diagrams, e.g., RED diagrams (the underlying symbolic representation in the model checker RED), have shown considerable performance enhancement in model-checking timed automata (TAs) and linear hybrid automata (LHAs). A RED diagram for a TA can represent the dense-time and discrete parts of TA states in a single and integrated decision diagram. In this work, we experiment to investigate whether such performance enhancement can be duplicated with PTA model-checking. Specifically, we propose a lightweight extension to RED diagrams to represent quantitative states of PTAs in an integrated manner, yet preserving the structure-sharing capacity of RED diagrams. We then develop and implement a symbolic reachability analysis algorithm for PTAs based on the extended RED diagrams. We further carry out experiments with the PTA benchmarks from a popular probabilistic model checker PRISM to evaluate the performance of such integrated decision diagrams and the reachability analysis algorithm. Experimental results show that our approach can indeed help to improve the time-efficiency and scalability of PTA model-checking.Keywords:
Binary decision diagram
Representation
Binary decision diagram (BDD) is a modern data structure proved to be compact in representation and efficient in manipulation of Boolean formulas. Using binary decision diagram in network reliability analysis has already been investigated by some researchers. In this paper we show how an exact algorithm for network reliability can be improved and implemented efficiently using CUDD - Colorado University decision diagram.
Binary decision diagram
Representation
Cite
Citations (7)
Timed automaton
Reachability problem
Enumeration
Cite
Citations (11)
Binary decision diagram
Symbolic trajectory evaluation
Abstraction model checking
Cite
Citations (24)
In this paper we introduce a new decision diagram based model, the 123-decision diagram, which can be used to efficiently synthesize DCVS circuits. We compare our approach to traditional DCVS synthesis techniques based on ordered binary decision diagrams(OBDDs) and show that our approach is guaranteed to perform as well as or better than OBDD based methods.
Binary decision diagram
Cite
Citations (4)
Reachability problem
Timed automaton
Cite
Citations (140)
Within the framework of time verification of real time systems, we present a new technique for the reachability analysis of hybrid automata. We call this technique the Splitting Reachability Analysis. It is applied to a synchronized product of hybrid automata. The basic idea is to compute separately and simultaneously states sets in each component of a synchronized product of hybrid automata. The composition of these sets is an upper-approximation of the reachable states set of the synchronized product. Compared to a classical technique, the benefit, shown through with the example of the Fischer mutual exclusion protocol, is to reduce the costs in memory and computation time.
Cite
Citations (1)
We present a new safety hardware model checker SimpleCAR that serves as a reference implementation for evaluating Complementary Approximate Reachability (CAR), a new SAT-based model checking framework inspired by classical reachability analysis. The tool gives a "bottom-line" performance measure for comparing future extensions to the framework. We demonstrate the performance of SimpleCAR on challenging benchmarks from the Hardware Model Checking Competition. Our experiments indicate that SimpleCAR is particularly suited for unsafety checking, or bug-finding; it is able to solve 7 unsafe instances within 1 h that are not solvable by any other state-of-the-art techniques, including BMC and IC3/PDR, within 8 h. We also identify a bug (reports safe instead of unsafe) and 48 counterexample generation errors in the tools compared in our analysis.
Counterexample
Cite
Citations (10)
In this paper we discuss the application of formal methods for the verification of properties of control systems designed for autonomous robotic systems. We illustrate our proposal in the context of surgery by considering the automatic execution of a simple action such as puncturing. To prove that a sequence of subtasks planned on pre-operative data can successfully accomplish the surgical operation despite model uncertainties, we specify the problem by using hybrid automata. We express the requirements of interest as questions about reachability properties of the hybrid automaton model. Then, we compare the different performance of current state-of-the art tools for reachability analysis of hybrid automata.
Hybrid automaton
Puncturing
Reachability problem
Sequence (biology)
Cite
Citations (3)
Reachability problem
Cite
Citations (9)
This paper proposes an algorithm to maximize reachability probabilities for rectangular automata with random clocks via a history-dependent prophetic scheduler. This model class incorporates time-induced nondeterminism on discrete behavior and nondeterminism in the dynamic behavior. After computing reachable state sets via a forward flowpipe construction, we use backward refinement to compute maximum reachability probabilities. The feasibility of the presented approach is illustrated on a scalable model.
Reachability problem
Cite
Citations (1)