=Paper=
{{Paper
|id=Vol-2571/CSP2019_paper_12
|storemode=property
|title= Checking MTL Properties of Timed Automata with Dense Time using Satisfiability Modulo Theories (Extended Abstract)
|pdfUrl=https://ceur-ws.org/Vol-2571/CSP2019_paper_12.pdf
|volume=Vol-2571
|authors=Agnieszka M. Zbrzezny,Andrzej Zbrzezny
|dblpUrl=https://dblp.org/rec/conf/csp/ZbrzeznyZ19
}}
== Checking MTL Properties of Timed Automata with Dense Time using Satisfiability Modulo Theories (Extended Abstract)==
https://ceur-ws.org/Vol-2571/CSP2019_paper_12.pdf
Checking MTL Properties of Timed Automata with
Dense Time using Satisfiability Modulo Theories
(Extended abstract)
Agnieszka M. Zbrzezny1 and Andrzej Zbrzezny2
1
Faculty of Mathematics and Computer Science, University of Warmia and Mazury in Olsztyn,
Poland, agnieszka.zbrzezny@matman.uwm.edu.pl
2
Institute of Mathematics and Computer Science, Jan Długosz University in Czȩstochowa,
Poland. a.zbrzezny@ujd.edu.pl
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 effi-
cient algorithmic and tool support. The timed automata formalism is now applied to
the analysis of timing analysis of software and asynchronous circuits [12] and real-
time 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 rep-
resenting 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 ver-
ification 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.
Copyright R 2019 for this paper by its authors. Use permitted under Creative Commons
License Attribution 4.0 International (CC BY 4.0).
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 in-
terpreted 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 exis-
tential 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 = {x0 , . . . , xn−1 } 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 IR|X | . For X ⊆ X , the
valuation v 0 = v[X := 0] is defined as: ∀x ∈ X, v 0 (x) = 0 and ∀x ∈ X \ X, v 0 (x) =
v(x). For δ ∈ IR, v + δ denotes the valuation v 00 such that ∀x ∈ X , v 00 (x) = v(x) + δ.
Let x ∈ X , c ∈ IN, and ∼ ∈ {<, 6, =, >, >}. 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 |= 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 ∈ Loc is an initial location,
– T ⊆ Loc × Act × C(X ) × 2X × Loc is a transition relation,
– X is a finite set of clocks,
– Inv : Loc 7→ C(X ) is a state invariant function,
– 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.
σ,cc,X
Each element t ∈ T is denoted by ` −→ `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 ∈ 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 , Inv, AP, V ) a timed automaton, and v 0 a
clock valuation such that ∀x ∈ X , v 0 (x) = 0.
A concrete model for A is a tuple MA = (Q, q 0 , −→, V), where
– Q = Loc × IRn s a set of the concrete states,
– q 0 = (`0 , v 0 ) is the initial state,
– −→⊆ Q × Q is a total binary relation on Q defined by action and time transitions
as follows. For a ∈ Act and δ ∈ IR+ ,
a a,cc,X
1. Action transition: : (`, v) −→ (`0 , v 0 ) iff there is a transition ` −→ `0 ∈ T
such that v |= cc ∧ Inv(`) and v 0 = v[X := 0] and v 0 |= Inv(`0 ),
δ
2. Time transition: (`, v) −→ (`, v + δ) iff v |= Inv(`) and v + δ |= Inv(`).
– V : Q 7→ 2AP is a valuation function such that V((`, v)) = V (`) for each state
(`, v) ∈ Q.
A run ρ in a concrete model for the timed automata A is a infinite sequence of
δ0 ,a0 δ1 ,a1 δ2 ,a2
concrete states q0 −→ q1 −→ q2 −→ . . . such that qi ∈ Q, ai ∈ Act and δi ∈ IR+ ,
for all i ∈ IN. An assumption that δi ∈ 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 q 0 exactly 3 time units later.
Syntax Let p ∈ AP be a propositional variable and I be an interval in IN of the form
[a, b) or [a, ∞), where a, b ∈ IN and a < b. The MTL logic in release positive normal
form is defined in the following way:
α := true | false | p | ¬p | α ∧ α | α ∨ α | αUI α | GI α.
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:
df df
FI α = true UI α αRI β = 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” seman-
tics [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 con-
tinuous 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, q 0 , −→, V) be a concrete model for the timed
δ a δ a δ a
0
automata A, ρ : q0 −→ q00 −→
0 1
q1 −→ q10 −→
1 2
q2 −→ q20 −→
2
. . . be a run in A, which
δ0 ,a0 δ1 ,a1 δ2 ,a2
can be written in the shorter way: ρ : q0 −→ q1 −→ q2 −→ . . .. 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)|=EMTL ϕ instead of
M, (λρ , m)|=EMTL ϕ, for each MTL formula ϕ.
Definition 3. Let α and β be MTL formulae. The satisfaction relation |=EMTL , which
indicates truth of an MTL formula in the concrete model MA along a path λρ starting
at position m ∈ IN, is defined inductively as follows:
(λρ , m) |=EMTL true,
(λρ , m) 6 |=EMTL false,
(λρ , m) |=EMTL p iff p ∈ V(ρ(m)),
(λρ , m) |=EMTL ¬p iff p 6∈ V(ρ(m)),
(λρ , m) |=EMTL α ∧ β iff (λρ , m) |=EMTL α and (λρ , m) |=EMTL β,
(λρ , m) |=EMTL α ∨ β iff (λρ , m) |=EMTL α or (λρ , m) |=EMTL β,
(λρ , m) |=EMTL αUI β iff (∃j ≥ m)(ζρ (j) − ζρ (m) ∈ I and (λρ , m + j) |=EMTL β
and (∀m 6 j 0 < j)(λρ , m + j 0 ) |=EMTL α),
(λρ , m)|=EMTL GI β iff (∀j ≥ m)(ζρ (j) − ζρ (m) ∈ I implies (λρ , m + j) |=EMTL β).
As (λρ , 0) = λρ , we shall write MA , λρ |=EMTL ϕ for MA , (λρ , 0) |=EMTL ϕ.
An MTL formula ϕ is existentially valid in the model MA , denoted MA |=EMTL Eϕ,
if, and only if MA , λρ |=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 (ζπel (0), ζπel (1), . . .).
4. After the translation to SMT, the SMT-solver checks 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,∞) (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,∞) (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,∞) (F[0,2·n+3) (ConsReceived)). It states that the Consumer infinitely
often is receiving the data in time less then 2 · n + 3.
Fig. 1: The TGPP system.
5.2 Timed Train Controller System
Fig. 2: The TTCS system.
The Timed Train Controller System (also known as Fischer’s mutual exclusion pro-
tocol) 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 en-
try 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.
Wn−1 Wn
– ψ1 = F[0,7) ( i=1 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
Wn valid in the model if and only if ∆ ≥ δ.
– ψ2 = G[0,∞) (F[0,9) ( 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 ofW ∆ and δ.
n
– ψ3 = F[0,∞) ( i=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 pro-
gramming 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 bench-
marks. 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 ob-
serve 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 formu-
lae the memory usage for BMC and SMT-solver is almost the same.
Total time usage for the TGPP
6000
φ1
φ2
5000 φ3
φ4
φ
4000 5
Time in sec.
3000
2000
1000
0
1 2 3 4 5 6 7 8 9 10
Number of Nodes
Fig. 3: Total time and usage for TGPP.
Total memory usage for the TGPP
300
φ1
φ2
250 φ3
φ4
φ
200 5
Memory in MB
150
100
50
0
1 2 3 4 5 6 7 8 9 10
Number of Nodes
Fig. 4: Total memory usage for TGPP.
BMC time usage for the TGPP SMT time usage for the TGPP
45 6000
φ1 φ1
φ φ2
40 φ2 φ3
3
φ4 5000 φ4
35 φ5 φ5
30 4000
Time in sec.
Time in sec.
25
3000
20
15 2000
10
1000
5
0 0
1 2 3 4 5 6 7 8 9 10 1 2 3 4 5 6 7 8 9 10
Number of Trains Number of Trains
Fig. 5: BMC and SMT time usage for TGPP.
BMC memory usage for the TGPP SMT memory usage for the TGPP
300 250
φ1 φ1
250 φ2 φ2
200 φ3
φ3
Memory in MB φ φ4
Memory in MB
200 φ4 φ
5 150 5
150
100
100
50 50
0 0
1 2 3 4 5 6 7 8 9 10 1 2 3 4 5 6 7 8 9 10
Number of Nodes Number of Nodes
Fig. 6: BMC and SMT memory usage for 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
ψ1
ψ2
6000 ψ3
5000
Time in sec.
4000
3000
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
Fig. 7: Total time usage for TTCS.
Fig. 7 shows the time usage for the verification process for all the formulae. We can
observe that the third formula could be verified only for the TTCS with 5 trains. We
tried to verify it for the system with 6 trains but we gave up after 6 hours. Fig. 8 shows
the memory usage for all the formulae.
Fig. 9 shows the time usage for BMC and SMT for all the formulae and TTCS.
For the formula ψ2 we can observe that BMC algorithm uses more time than the SMT-
solver. However, the plot for this formula and SMT looks a bit weird. We expect that
with the scaling up the benchmark the time usage would be bigger. For 120 and 130
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
1800
ψ1
ψ
1600 ψ2
3
1400
1200
Memory in MB
1000
800
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
Fig. 8: Total memory usage for TTCS.
BMC time usage for the TTCS SMT time usage for the TTCS
5000 3000
ψ1 ψ1
4500 ψ2 ψ2
ψ3 ψ3
2500
4000
3500
2000
Time in sec.
Time in sec.
3000
2500 1500
2000
1000
1500
1000
500
500
0 0
2 3 4 5 10 20 30 40 50 60 70 80 90 100 110 120 130 140 145 2 3 4 5 10 20 30 40 50 60 70 80 90 100 110 120 130 140 145
Number of Trains Number of Trains
Fig. 9: SMT and BMC time usage for TTCS.
BMC memory usage for the TTCS SMT memory usage for the TTCS
1800 1100
ψ1 ψ1
ψ 1000 ψ2
1600 ψ2 ψ3
3
900
1400
800
1200
700
Memory in MB
Memory in MB
1000 600
800 500
400
600
300
400
200
200 100
0 0
2 3 4 5 10 20 30 40 50 60 70 80 90 100 110 120 130 140 145 2 3 4 5 10 20 30 40 50 60 70 80 90 100 110 120 130 140 145
Number of Trains Number of Trains
Fig. 10: SMT and BMC memory usage for TTCS.
6 Conclusions
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 exper-
imentally 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 the-
ories problem.
In the future we would like to develop a corresponding SAT-based method. Devel-
oping 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 In-
formation 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. Woź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 Sys-
tems, 2(4):255–299, 1990.
17. W. Penczek, B. Woźna, and A. Zbrzezny. Bounded model checking for the universal frag-
ment 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 com-
plexity 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 Quan-
titative 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 au-
tomata. 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. Woźna-Szcześniak and A. Zbrzezny. Checking MTL properties of discrete timed au-
tomata via bounded model checking. Fundam. Inform., 135(4):553–568, 2014.
23. Bożena Woźna-Szcześ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 dis-
crete timed automata (extended abstract). In Proceedings of the 25th International Work-
shop on Concurrency, Specification and Programming, Rostock, Germany, September 28-30,
2016., pages 37–48, 2016.