-
Notifications
You must be signed in to change notification settings - Fork 18
Zone graphs in TChecker
Foreword: this document describes zone graphs in TChecker tools v0.3 and above. Zone graphs in previous versions were defined similarly, except that the API may differ.
Zone graphs give a semi-symbolic definition of the semantics of timed automata. Their definition is based on the semantics of timed automata. Zone graphs allow to manipulate clock valuations symbolically while locations and integer variables are enumerated.
Zone graphs represent (infinite) sets of clock valuations symbolically using zones. A zone is a set of clock valuations that is described by a conjunction of constraints of the form x # c and x - y # c where x and y are clocks, # is an comparison operator among <, <=, =, >= and >, and c is an integer.
Formally, a node of a zone graph is of the form (L,V,Z) where L is a tuple of locations, V is a valuation of the bounded integer variables in the model, and Z is a zone. An initial node is a tuple (L, V, Z) where L is a tuple of initial locations, V maps each bounded integer variable to its initial value, and Z consists of the clock valuation that maps each clock to 0.
There are two kind of edges in the zone graph. There is a discrete edge (L,V,Z) ~~E~> (L',V',Z') if Z' is the set of clock valuations X' such that there is a discrete transition (L,V,X) --E-> (L',V',X') for some clock valuation X in Z, and Z' is not empty. There is a timed edge (L,V,Z) ~~~> (L,V,Z') if Z' is the set of clock valuations X' such that there is a timed transition (L,V,X) ---> (L,V,X') for some clock valuation X in Z.
It can be shown that the semi-symbolic semantics induced by zone graphs is sound and complete. To every finite or infinite path in the zone graph corresponds a run (sequence of transitions) of the automaton. And conversely, to every finite or infinite run of the automaton corresponds a path in the zone graph.
The definition of zone graphs above is quite frequent in the literature. However, this is not how zone graphs are implemented in verification tools. Indeed, using this definition would generate zone graphs with many useless nodes. In particular, it can be observed that for timed edges (L,V,Z) ~~~> (L,V,Z'), the zone Z is included in the zone Z'. Keeping only the bigger zone Z' is sufficient as Z does not add any new behavior. Thus implementations prefer to work with edges that combine a discrete transition and a timed transition. There are two ways to do so.
The name comes from the fact that this is how zone graphs have first been implemented. In this approach:
- initial nodes are defined as before
- edges consists in a timed edge followed by a discrete edge. Formally: there is a transition (L,V,Z) ==E=> (L',V',Z') if (L,V,Z) ~~~> (L,V,Z'') ~~E~> (L',V',Z') for some zone Z''.
Standard zone graphs can be created in TChecker using tchecker::zg::factory with value tchecker::zg::STANDARD_SEMANTICS for the semantics.
This semantics makes the opposite choice: edges consists of a discrete edge first, followed by a timed edge. In details:
- initial nodes are of the form (L,V,Z) where L is a tuple of initial locations, V maps every bounded integer variable to its initial value, and Z is the zone
$\bigwedge_{clock \ x} (x >= 0)$ (i.e. the set of clock valuations that are reachable through timed transitions from the clock valuation that maps each clock to 0). - edges consists in a discrere edge followed by a timed edge. Formally: there is a transition (L,V,Z) ==E=> (L',V',Z') if (L,V,Z) ~~E~> (L',V',Z'') ~~~> (L,V,Z') for some zone Z''.
Elapsed zone graphs can be created in TChecker using tchecker::zg::factory with value tchecker::zg::ELAPSED_SEMANTICS for the semantics.
We start with an example to illustrate the differences between the two definitions. Let us consider a timed automaton with one clock x, no integer variable (they have no impact on the zone part), and two transitions:
--- (x<10), a -> l1
|
-> l0
|
--- (x>10), b -> l2
Let us first draw the standard zone graph:
=== a => (l1, x<10)
||
-> (l0, x>=0)
||
=== b => (l2, x>10)
On the other hand, the picture below represents the elapsed zone graph. Please recall, that delays (timed transitions) follow the discrete transitions, hence the difference in location l1 w.r.t the standard zone graph.
=== a => (l1, x>=0)
||
-> (l0, x>=0)
||
=== b => (l2, x>10)
Although the zone graphs may contain different zones, they are equivalent. More precisely, for every finite or infinite path in the standard zone graph, there exist a corresponding path in the elapsed zone graph, and conversely.
As a result, one can use any of them for verification purposes. Most of TChecker tools use elapsed zone graphs. There are two main reasons for that. On the one hand, many verification algorithms for timed automata only keep the nodes with maximal zones in memory. The elapsed semantics seems more promising, but it is not guaranteed to yield the smallest number of maximal nodes (in particular when timed automata have invariants). On the other hand some optimisations such as the aLU abstraction are optimal on the elapsed zone graph, but not on the standard zone graph.
Notice however that TChecker simulator tck-simulate works with the standard zone graph as it is more intuitive.
Zone graphs (with either semantics) are usually infinite. Extrapolations and abstractions are used in order to guarantee finiteness of the zone graphs (hence termination of verification algorithms).
The basic idea behind abstractions is to replace zones Z by sets of valuations W to build an abstract zone graph such that:
- there is only finitely many sets of valuations
W, which entails the finiteness of the abstract zone graph - to every finite or infinite path in the zone graph corresponds a path in the abstract zone graph, and conversely (soundness and completeness).
TChecker tools use extrapolations and abstractions to ensure termination of verification algorithms. Hence, TChecker outputs abstract zones, which contain unreachable valuations (although they preserve paths). To illustrate, the abstract zone graph on the previous example is depicted below. For this simple example, we get the same abstract zone graph using the standard semantics and the elapsed semantics, but it is not always the case.
=== a => (l1, x>=0)
||
-> (l0, x>=0)
||
=== b => (l2, x>=0)
TChecker simulation tool tck-simulate does not use any extrapolation/abstraction as it is not needed (simulations terminate by nature).
Please, refer to the following papers for details on extrapolations and abstractions for timed automata, as well as how they can be used in verification algorithms.
- Gerd Behrmann, Patricia Bouyer, Kim Guldstrand Larsen, Radek Pelánek: Lower and upper bounds in zone-based abstractions of timed automata. Int. J. Softw. Tools Technol. Transf. 8(3): 204-215 (2006)
- Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz: Better abstractions for timed automata. Inf. Comput. 251: 67-90 (2016)
- Paul Gastin, Sayan Mukherjee, B. Srivathsan: Reachability for Updatable Timed Automata Made Faster and More Effective. FSTTCS 2020: 47:1-47:17
The local-time semantics has been introduced in: Johan Bengtsson, Bengt Jonsson, Johan Lilius, Wang Yi: Partial Order Reductions for Timed Systems. CONCUR 1998: 485-500, and used for the (efficient) verification of systems with concurrent timed processes.
In this settings, each process in the system has its own time line. The time lines of processes are synchronized when they perform a common action. Moreover, the time lines of the processes are also synchronized at the end of a run. With these two constraints, we can show that local-time zone graphs are equivalent to zone graphs: for every finite path in the local-time zone graph, there exists a corresponding path in the zone graph and conversely.
Local-time zone graphs are called refzg (zone graph with reference clocks) in TChecker. They generalize zone graphs in the sense that every path in the zone graph is also a path in the local-time zone graph. Local-time zone graphs are created using the factory tchecker::refzg::factory. As for zone graph, two semantics are provided: the standard one (specified with tchecker::refzg::STANDARD_SEMANTICS) and the elapsed one (specified with tchecker::refzg::ELAPSED_SEMANTICS). They are defined as for zone graphs, except that the semantics of discrete and timed transitions is adapted to the local time settings.
There is no extrapolation in the local-time settings. However, abstractions sync-aLU and aLU* have been defined to ensure termination of reachability algorithms. These notions have also been extended to the case of infinite runs. Please refer to the following publications for details:
- R. Govind, Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz:Revisiting Local Time Semantics for Networks of Timed Automata. CONCUR 2019: 16:1-16:15
- R. Govind, Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz: Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods. LICS 2022: 24:1-24:14
- Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz: Checking Timed Büchi Automata Emptiness Using the Local-Time Semantics. CONCUR 2022: 12:1-12:24