Dependency graphs with applications to verification
- PDF / 1,149,649 Bytes
- 20 Pages / 595.276 x 790.866 pts Page_size
- 35 Downloads / 182 Views
STTT Special Issue: SPIN 2019
Dependency graphs with applications to verification Søren Enevoldsen1 · Kim G. Larsen1 · Anders Mariegaard1 · Jiˇrí Srba1
© Springer-Verlag GmbH Germany, part of Springer Nature 2020
Abstract Dependency graphs, as introduced more than 20 years ago by Liu and Smolka, are oriented graphs with hyperedges that connect nodes with sets of target nodes in order to represent causal dependencies in the graph. Numerous verification problems can be reduced into the problem of computing a minimum or maximum fixed-point assignment on dependency graphs. In the original definition, assignments link each node with a Boolean value; however, in the recent work the assignment domains have been extended to more general setting, even including infinite domains. In this survey paper, we present an overview of the recent results on extensions of dependency graphs in order to deal with verification of quantitative, probabilistic, parameterized and timed systems. Keywords Dependency graphs · Verification · Fixed-point computation · On-the-fly algorithms
1 Model verification The scale of computational systems nowadays varies from simple toggle-buttons to various embedded systems and network routers up to complex multi-purpose computers. In safety critical applications, we need to provide guarantees about system behaviour in all situations/configurations that the system can encounter. Such guarantees are classically provided by first creating a formal model of the system (at an appropriate abstraction level) and then using formal methods such as model checking and equivalence checking to rigorously argue about the behaviour of the models. At the highest abstraction level, systems are usually modelled as labelled transition systems or Kripke structures (see [8] for an introduction). In labelled transition systems (LTSs), a process changes its (unobservable) internal states by performing visible actions. Kripke structures, on the other hand, allow to observe the validity of a number of atomic predicates revealing some (partial) information about the current state of a given process, whereas the state changes are not labelled by any visible actions.
B 1
Jiˇrí Srba [email protected]
An example of LTS modelling a simple traffic light is given in Fig. 1a. Although the states are named for convenience, they are considered opaque. Instead, this formalism uses the action-based perspective where the actions of the transitions are considered visible. For example from R1 , there is a transition to R1 labelled with a ‘wait’ action that allows to extend the duration of the red colour, after which only the action ‘to green’ is available. A slight variant of the LTS is given in Fig. 1b where from G 2 it is possible to enter directly the state R2 by performing the ‘to red’ action. We can now ask the (equivalence checking) question whether the two systems are equivalent up to some given notion of behavioural equivalence [50], e.g. bisimilarity [46], which is not the case in our example. The simple traffic light can also be
Data Loading...
