Checking MTL Properties of Timed Automata with Dense Time using Satisfiability Modulo Theories (Extended abstract)

Abstract

We investigate a new SMT-based bounded model checking (BMC) method for the existential part of Metric Temporal Logic (MTL). The MTL logic is interpreted over linear dense infinite time models generated by timed automata with dense time. We implemented the new SMT-based bounded model checking technique for MTL and as a case study we applied the technique to the analysis of the Timed Generic Pipeline Paradigm and Timed Train Controller System, both modelled by a network of timed automata.

1 Introduction

Timed automata [ 2 ] are very convenient for modelling and reasoning about real-time systems: they combine a powerful formalism with advanced expressiveness and efficient algorithmic and tool support. The timed automata formalism is now applied to the analysis of timing analysis of software and asynchronous circuits [ 12 ] and realtime control programs [ 13 ]. Timed automata technology was also used to analysis of numerous real-time communication protocols [ 20 ].

Timed automata (TA) are adequate to represent systems, but not that much for representing properties of systems3. Temporal logics are a well known framework in the field of specification and verification of computer systems [ 18 ]. Linear Temporal Logic (LTL) allows to express properties about each individual execution of a system, such as the fact that any occurrence of a problem eventually triggers the alarm. Real-time constraints have naturally been added to temporal logics [ 16, 1 ] at the beginning of the 90s. The resulting logics allow to express e.g. that any occurrence of a problem in a system will trigger the alarm within at most 5 time units.

Metric Temporal Logic (MTL) [ 16 ] was discussed in the literature e.g on the verification of real-time systems [ 14, 11, 22, 19, 7 ]. MTL extends the until and globally 3 Assume that one TA represents a system and the second TA represents a property of the system. We would like to check if TA representing the system satisfies the property. This problem is unfortunately undecidable for timed automata. operators of classical temporal logic with an interval which specifies the time interval within which the formula must be satisfied. The MTL logic has traditionally been interpreted in two ways: the pointwise and the continuous semantics. In this paper we are focused on the pointwise version. The temporal assertions are interpreted only at time points where an action happens in the observed timed behaviour of a system.

Bounded model checking [ 8, 9, 17 ] (BMC) is one of the symbolic model checking technique designed for finding witnesses for existential properties or counterexamples for universal properties. Its main idea is to consider a model reduced to a specific depth. The method works by mapping a bounded model checking problem to the Boolean satisfiability problem (SAT) or to satisfiability modulo theories problem (SMT).

The satisfiability and model checking problems for MTL are undecidable over the interval-based semantics [ 5 ]. This has led to consider various restrictions on MTL to recover decidability [ 21, 22, 3 ]. The main steps of our new method for MTL and timed automata with dense time can be described as follows: 1. the timed model (infinite) is reduced to a finite model, 2. the MTL formula is translated to LTLq formula [ 24, 25 ], 3. since the interval modalities in MTL appear as literals in LTLq formula, the existential properties are reduced to a satisfiability modulo theories problem (SMT).

We evaluate the new BMC method experimentally by means of a timed generic pipeline paradigm (TGPP) and timed train controller system, which are modelled by a network of timed automata with dense time. 2

Timed Automata

The model of timed automata has been defined in the 90s by Alur and Dill as a model for representing systems with real-time constraints. A timed automaton is basically a finite automaton which manipulates finitely many variables called clocks.

We assume a finite set X = fx0; : : : ; xn 1g of variables, called clocks. A clock valuation is a total function v : X 7! IR that assigns to each clock x a non-negative real value v(x). The set of all the clock valuations is denoted by IRjX j. For X X , the valuation v0 = v[X := 0] is defined as: 8x 2 X, v0(x) = 0 and 8x 2 X n X, v0(x) = v(x). For 2 IR, v + denotes the valuation v00 such that 8x 2 X ; v00(x) = v(x) + . Let x 2 X , c 2 IN, and 2 f<; 6; =; >; >g. A guard over X is a finite conjunction of expressions of the form x c. We denote by C(X ) the set of guards over X . A clock valuation v satisfies a clock guard cc, written as v j= cc, iff cc evaluates to true using the clock values given by the valuation v.

Definition 1. A timed automaton is a tuple A = (Act; Loc; `0; T; X ; Inv; AP; V ), where – Act is a finite set of actions, – Loc is a finite set of locations, – `0 2 Loc is an initial location, – T Loc Act C(X ) 2X – X is a finite set of clocks, – Inv : Loc 7! C(X ) is a state invariant function,

Loc is a transition relation, – AP is a set of atomic proposition, and – V : Loc 7! 2AP is a valuation function assigning to each location a set of atomic propositions true in this location.

Each element t 2 T is denoted by ` ;c!c;X `0, and it represents a transition from location ` to location `0 on the input action . X X is the set of the clocks to be reset with this transition, and cc 2 C(X ) is the enabling condition for t. 2.1

Concrete model

The semantics of the timed automaton is defined by associating a transition system with it, which we call a concrete model.

Definition 2. Let A = (Act; Loc; `0; T ; X ; I nv; AP ; V ) a timed automaton, and v0a clock valuation such that 8x 2 X , v0(x) = 0.

A concrete model for A is a tuple MA = (Q; q0; !; V ), where – Q = Loc IRn s a set of the concrete states, – q0 = (`0; v0) is the initial state, – ! Q Q is a total binary relation on Q defined by action and time transitions as follows. For a 2 Act and 2 IR+, 1. Action transition: : (`; v) a! (`0; v0) iff there is a transition ` a;c!c;X `0 2 T such that v j= cc ^ I nv(`) and v0 = v[X := 0] and v0 j= I nv(`0), 2. Time transition: (`; v) ! (`; v + ) iff v j= I nv(`) and v + j= I nv(`). – V : Q 7! 2AP is a valuation function such that V ((`; v)) = V (`) for each state (`; v) 2 Q.

A run

in a concrete model for the timed automata A is a infinite sequence of concrete states q0 0!;a0 q1 1!;a1 q2 2!;a2 : : : such that qi 2 Q, ai 2 Act and i 2 IR+, for all i 2 IN. An assumption that i 2 IR+ implies that runs are strongly monotonic. This is because the definition of the run does not permit two consecutive actions to be performed one after the other, i.e., between each two actions some time must pass. 3

MTL logic

MTL logic [ 16 ] (metric LTL) is a timed temporal logic with interval operators. It has received much attention in the literature on the verification of real-time systems. MTL can express many time constraints. For example we can express a system property: if a system is in the state q, than it will be in the state q0 exactly 3 time units later. Syntax Let p 2 AP be a propositional variable and I be an interval in IN of the form [a; b) or [a; 1), where a; b 2 IN and a < b. The MTL logic in release positive normal form is defined in the following way: := true j false j p j :p j ^ j _ j

Intuitively, UI and GI are the operators for, respectively, bounded until and bounded always and they are ridden as, respectively, „until in the interval I” and „always in the interval I”. The operators FI and RI are defined in the standard way:

FI d=f true UI

RI df = GI _

UI( _ ).

Semantics Over dense time the logic has traditionally been interpreted in either of two ways which have come to be known as the “pointwise” and the “continuous” semantics [ 10 ]. In the pointwise approach temporal assertions are interpreted only at time points where action happens in the observed timed behaviour of a system. In the continuous one is allowed to assert formulae at arbitrary time points between actions as well.

In the presented method we use the pointwise semantics.

Let A be a time automata, MA = (Q; q0; !; V) be a concrete model for the timed automata A, : q0 !0 q00 a!0 q1 !1 q10 a!1 q2 !2 q20 a!2 : : : be a run in A, which can be written in the shorter way: : q0 0!;a0 q1 1!;a1 q2 2!;a2 : : :. Each of the runs determines the path : q0; q00; q1; q10; q2; q20 : : : in an unambiguous way. Given a run one can define a function : IN 7! IR+ such that, for all the position j > 0, (j) is a sum of all the time transitions along the run till the position j. For all j > m, the function (j) returns the value of the global time (in [ 10 ] called „duration”).

To make the definition more clear we use a notation ( ; m)j=EMTL' instead of M; ( ; m)j=EMTL', for each MTL formula '.

Definition 3. Let and be MTL formulae. The satisfaction relation j=EMTL, which indicates truth of an MTL formula in the concrete model MA along a path starting at position m 2 IN, is defined inductively as follows: ( ; m) j=EMTL true, ( ; m) 6 j=EMTL false, ( ; m) j=EMTL p iff p 2 V( (m)), ( ; m) j=EMTL :p iff p 62 V( (m)), ( ; m) j=EMTL ^ iff ( ; m) j=EMTL ( ; m) j=EMTL _ iff ( ; m) j=EMTL ( ; m) j=EMTL UI iff (9j m)( (j) and (8m 6 j0 < j)( ; m + j0) j=EMTL ), ( ; m)j=EMTL GI iff (8j m)( (j) and ( ; m) j=EMTL , or ( ; m) j=EMTL ,

(m) 2 I and ( ; m + j) j=EMTL (m) 2 I implies ( ; m + j) j=EMTL ).

As ( ; 0) = , we shall write MA; j=EMTL ' for MA; ( ; 0) j=EMTL '. An MTL formula ' is existentially valid in the model MA, denoted MA j=EMTL E', if, and only if MA; j=EMTL ' for some path starting in the initial state of MA. Determining whether an MTL formula ' is existentially valid in a given model is called an existential model checking problem. 4

SMT-based bounded model checking

The verification method presented in this paper is based on the translation of MTL formulae to LTLq formulae defined in [ 24, 25 ]. We do not report on this step here in detail, since it requires introducing the huge mathematical machinery, but in fact it can be done in a way similar to the one presented in [ 24 ]. However, this will be provided in the full version of the paper. We refer the reader to the chapter 4 of the thesis [ 24 ] for details.

The SMT-based bounded model checking can be described in the following steps: 1. Since the concrete model is infinite we have to abstract the model to be able to applied bounded model checking technique. It is a well-known technique [ 15, 4 ]. 2. We use the EMTL semantics in the abstract model [ 24 ] and translate the EMTL formula into an LTLq formula. 3. The next step is standard. It consists of a translation of the transition relation in the depth k in the abstract model and the LTLq formula into satisfiability modulo theories problem. The difference between the BMC method for classic LTL and our method lies in encoding of a finite prefix ( l (0); l (1); : : :). 4. After the translation to SMT, the SMT-solveer checkes the satisfiability of the LTLq formula in the abstract model. 5

Experimental results

In this section we experimentally evaluate the performance of our new translation. We have conducted the experiments using the slightly modified timed generic pipeline paradigm (TGPP) and timed train controller system (TTCS) [ 23 ]. 5.1

Timed Generic Pipeline Paradigm

The Timed Generic Pipeline Paradigm (TGPP) timed automata model shown in Figure 1 consists of a Producer producing data within the certain time interval ([a; b]) or being inactive, a Consumer receiving data within the certain time interval ([c; d]) or being inactive within the certain time interval ([g; h]), and a chain of n intermediate Nodes which can be ready for receiving data within the certain time interval ([c; d]), processing data within the certain time interval ([e; f ]) or sending data. We assume that a = c = e = g = 1 and b = d = f = h = 2 n + 2, where n represents a number of nodes in the TGPP.

To compare our experimental results with [ 23 ], we have tested the TGPP timed automata model, scaled in the number of intermediate nodes on the following MTL formulae that existentially hold in the model of TGPP (n is the number of nodes): – '1 = F[0;2 n+3)(ConsReceived). It expresses that Consumer receives the data in at most 2 n + 3 time units. – '2 = G[0;2 n+2)(ConsReady). It states that the Consumer is always forced to receive the data in 2 n + 2 time units. – '3 = G[0;1)(P rodReady _ConsReady). It states that always either the Producer has sent the data or the Consumer has received the data. – '4 = F[0;2 n+3)(G[0;1)(P rodSend _ ConsReceived)). It states that eventually in time less then 2 n + 3 it is always the case that the Producer is ready to send the data or the Consumer has received the data. – '5 = G[0;1)(F[0;2 n+3)(ConsReceived)). It states that the Consumer infinitely often is receiving the data in time less then 2 n + 3.

The Timed Train Controller System (also known as Fischer’s mutual exclusion protocol) consists of n (for n 2) trains T1; : : : ; Tn, each one using its own circular track for travelling in one direction and containing its own clock xi, together with controller C used to coordinate the access of trains to the tunnel through which all trains have to pass at certain point. There is only one track in the tunnel, so trains arriving from each direction cannot use it in this same time. There are signals on both sides of the tunnel, which can be either red or green. All trains notify the controller when they request entry to the tunnel or when they leave the tunnel. The controller controls the colour of the displayed signal, and the behaviour of the scenario depends on the values and ( makes it incorrect - the mutual exclusion does not hold).

Controller C has n + 1 states, denoting that all trains are away (state 0), and the numbers of trains, i.e., 1; : : : ; n. Controller C is initially at state 0. The action Starti of train Ti denotes the passage from state away to the state where the train wishes to obtain access to the tunnel. This is allowed only if controller C is in state 0. Similarly, train Ti synchronises with controller C on action approachi, which denotes setting C to state i, as well as outi, which denotes setting C to state 0. Finally, action ini denotes the entering of train Ti into the tunnel.

– – – 1 = F[0;7)(Win=11 Wn

j=i+1(tunneli ^tunnelj )). It states that the mutual exclusion property is violated, i.e. for some path some two trains are in the tunnel at the same time. The formula is existentially valid in the model if and only if . 2 = G[0;1)(F[0;9)(Wn

i=1(tunneli))). It states that always eventually some of the trains enters the tunnel. The formula is existentially valid in the model regardless of the values of and .

3 = F[0;1)(Win=1(tunneli)). It states that eventually all the trains are in the tunnel. The formula is existentially valid in the model if ndonlyif . 5.3

Performance evaluation

We have performed our experimental results on a computer equipped with I7-5500U processor, 12 GB of RAM, and the operating system Linux with the kernel 5.2.9. Our SMT-based BMC algorithm is implemented as standalone programs written in the programming language C++. We used the state of the art SMT-solver Z3 (program version 8.4.5).

TGPP

The number of considered k-paths (fk) for the translation is always equal to 1. The length of the witness for the formula '1 is equal to 4 (n + 1) ; for the formula '2 is equal to 8 n + 6; for the formula '3 and is equal to 8 n + 6; for the formula '4 is equal to 8 n + 15; for the formula '5 is equal to 8 n + 6.

The experimental results presented on the Fig. 3 show total time usage. We can observe that the SMT-based method is sensitive to scaling up the size of the benchmarks. For more complicated formulae time usage grows very fast with the size of the benchmark.

The maximum memory usage for all the formulae showed on the Fig. 4 is not very big. The biggest memory usage was for the formula '5 and it amounts 375 MB.

Fig. 5 shows time usage for bounded model checking algorithm ( translation of the model and the formula to SMT format) and for the SMT-solver. We can observe that almost the whole time were consumed by the SMT-solver (the y axis has different scale on both figures). Generating a quantifier-free first-order formula in every case took less than 45 sec.

Fig. 6 shows memory usage for the BMC algorithm and SMT-solver. We can observe that for the formulae '1 and '3 the BMC algorithm did not use a lot of memory and the SMT-solver consumed almost the whole memory in this case. For other formulae the memory usage for BMC and SMT-solver is almost the same.

Total time usage for the TGPP 5

6

Number of Nodes 2 3 4 7 8 9 10

BMC memory usage for the TGPP

SMT memory usage for the TGPP

TTCS

As we mentioned before, the number of considered k-paths (fk) for the translation is always equal to 1. The length of the witness for the formula 1 is equal to 12 and for the formula 2 is equal to 7. For the formula 3 the length of the witness is equal to 12 for two trains, 18 for three trains, 32 for four trains, and 38 for five trains.

Total time usage for the TTCS 7000 ψψ21 6000 ψ3 5000 .ce 4000 s n i iem3000 T 2000 1000 0 2 3 4 5 10 20 30 40 50 60 70 80 90 100 110 120 130 140 145

Number of Trains trains we have the opposite situation. The reason of this situation is the heuristic of the SMT-solver. Z3 solver found the valuation faster. We think that the interesting future work will be finding the optimal SMT file for SMT-solvers [ 6 ].

Total memory usage for the TTCS

1 1600 ψψ3

2 1400 1200 B inM1000 y rom 800 e M 600 400 200 0 2 3 4 5 10 20 30 40 50 60 70 80 90 100 110 120 130 140 145

Number of Trains 0 2 3 4 5 10 20 30 40 50 60 70 80 90 100110120130140145

Number of Trains 0 2 3 4 5 10 20 30 40 50 60 70 80 90 100110120130140145

Number of Trains

Fig. 9: SMT and BMC time usage for TTCS.

BMC memory usage for the TTCS 0 2 3 4 5 10 20 30 40 50 60 70 80 90 100110120130140145

Number of Trains

SMT memory usage for the TTCS We have implemented and experimentally evaluated an SMT-based BMC method for real-time systems, which are modelled by timed automata with dense time, and for properties expressible in MTL with the semantics over timed automata. We have experimentally evaluated the method. The method is based on a translation of the existential model checking for MTL to the existential model checking for LTLq, and then on the translation of the existential model checking for LTLq to the satisfiability modulo theories problem.

In the future we would like to develop a corresponding SAT-based method. Developing the SMT-based method as a first method was a natural way to solve the problem. SMT encoding is easier to implement. However, the SAT encoding in many cases is more precise, what may give better experimental results.

References

1. R. Alur , C. Courcoubetis , and D. Dill . Model checking in dense real-time . Information and Computation , 104 ( 1 ): 2 - 34 , 1993 .

2. R. Alur and D. Dill . A theory of Timed Automata . Theoretical Computer Science , 126 ( 2 ): 183 - 235 , 1994 .

3. Rajeev Alur , Tomás Feder, and Thomas A. Henzinger . The benefits of relaxing punctuality . J. ACM , 43 ( 1 ): 116 - 146 , 1996 .

4. Rajeev Alur , Limor Fix, and Thomas A. Henzinger . Event-clock automata: A determinizable class of timed automata . Theor. Comput. Sci. , 211 ( 1-2 ): 253 - 273 , 1999 .

5. Rajeev Alur and Thomas A. Henzinger . Real-time logics: Complexity and expressiveness . In Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90) , Philadelphia, Pennsylvania, USA, June 4-7, 1990 , pages 390 - 401 , 1990 .

6. Mislav Balunovic , Pavol Bielik, and Martin T. Vechev . Learning to solve SMT formulas . In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018 , NeurIPS 2018 , 3 -8 December 2018 , Montréal, Canada., pages 10338 - 10349 , 2018 .

7. Stefano Baratella and Andrea Masini . A two-dimensional metric temporal logic . CoRR , abs/ 1903 .05894, 2019 .

8. A. Biere , A. Cimatti , E. Clarke, and Y. Zhu . Symbolic model checking without BDDs . In Proc. of the 5th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99) , volume 1579 of LNCS , pages 193 - 207 . Springer-Verlag, 1999 .

9. Armin Biere , Alessandro Cimatti, Edmund M. Clarke , Ofer Strichman, and Yunshan Zhu . Bounded model checking . Advances in Computers , 58 : 117 - 148 , 2003 .

10. P. Bouyer . Model-checking timed temporal logics . Electr. Notes Theor. Comput. Sci. , 231 : 323 - 341 , 2009 .

11. Patricia Bouyer , Fabrice Chevalier, and Nicolas Markey . On the expressiveness of TPTL and MTL . Inf. Comput., 208 ( 2 ): 97 - 116 , 2010 .

12. Marius Bozga , Jianmin Hou, Oded Maler, and Sergio Yovine . Verification of asynchronous circuits using timed automata . Electr. Notes Theor. Comput. Sci. , 65 ( 6 ): 47 - 59 , 2002 .

13. Henning Dierks . Plc-automata: a new class of implementable real-time automata . Theor. Comput. Sci. , 253 ( 1 ): 61 - 93 , 2001 .

14. Deepak D'Souza and Pavithra Prabhakar . On the expressiveness of MTL in the pointwise and continuous semantics . STTT , 9 ( 1 ): 1 - 4 , 2007 .

15. M. Kacprzak , W. Nabialek , A. Niewiadomski , W. Penczek , A. Pólrola , M. Szreter , B. Woz´na, and A. Zbrzezny . VerICS 2007 - a model checker for knowledge and real-time . Fundamenta Informaticae , 85 ( 1-4 ): 313 - 328 , 2008 .

16. Ron Koymans . Specifying real-time properties with metric temporal logic . Real-Time Systems , 2 ( 4 ): 255 - 299 , 1990 .

17. W. Penczek , B. Woz´na, and A. Zbrzezny . Bounded model checking for the universal fragment of CTL . Fundamenta Informaticae , 51 ( 1-2 ): 135 - 156 , 2002 .

18. A. Pnueli . The temporal logic of programs . In 18th Annual Symposium on Foundations of Computer Science , Providence, Rhode Island, USA, 31 October - 1 November 1977 , pages 46 - 57 , 1977 .

19. Vladislav Ryzhikov , Przemyslaw Andrzej Walega, and Michael Zakharyaschev . Data complexity and rewritability of ontology-mediated queries in metric temporal logic under the event-based semantics . In Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019 , Macao, China, August 10-16 , 2019 , pages 1851 - 1857 , 2019 .

20. Mathijs Schuts , Feng Zhu, Faranak Heidarian, and Frits W. Vaandrager . Modelling clock synchronization in the chess gmac WSN protocol . In Proceedings First Workshop on Quantitative Formal Methods: Theory and Applications , QFM 2009 , Eindhoven, The Netherlands, 3rd November 2009 ., pages 41 - 54 , 2009 .

21. Thomas Wilke . Specifying timed state sequences in powerful decidable logics and timed automata. In Formal Techniques in Real-Time and Fault-Tolerant Systems , Third International Symposium Organized Jointly with the Working Group Provably Correct Systems - ProCoS , Lübeck, Germany, September 19-23, Proceedings, pages 694 - 715 , 1994 .

22. B. Woz´na-Szczes´niak and A. Zbrzezny . Checking MTL properties of discrete timed automata via bounded model checking . Fundam . Inform., 135 ( 4 ): 553 - 568 , 2014 .

23. Boz ˙ena Woz´na-Szczes´niak and Andrzej Zbrzezny. Checking MTL properties of discrete timed automata via bounded model checking . Fundam . Inform., 135 ( 4 ): 553 - 568 , 2014 .

24. Agnieszka Zbrzezny . Selected SAT- and SMT-based model checking methods . PhD thesis , Institue of Computer Science, Polish Academy of Sciences, 2017 .

25. Agnieszka Zbrzezny and Andrzej Zbrzezny . Simple bounded MTL model checking for discrete timed automata (extended abstract) . In Proceedings of the 25th International Workshop on Concurrency, Specification and Programming , Rostock, Germany, September 28-30 , 2016 ., pages 37 - 48 , 2016 .