Games for the Verification of Timed Systems
Vinayak Prabhu
EECS Department, University of California, Berkeley
Technical Report No. UCB/EECS-2008-97
August 15, 2008
http://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-97.pdf
Models of timed systems must incorporate not only the sequence of system events, but the timings of these events as well to capture the real-time aspects of physical systems. Timed automata are models of real-time systems in which states consist of discrete locations and values for real-time clocks. The presence of real-time clocks leads to an uncountable state space. This thesis studies verification problems on timed automata in a game theoretic framework.
For untimed systems, two systems are close if every sequence of events of one system is also observable in the second system. For timed systems, the difference in timings of the two corresponding sequences is also of importance. We propose the notion of bisimulation distance which quantifies timing differences; if the bisimulation distance between two systems is epsilon, then (a) every sequence of events of one system has a corresponding matching sequence in the other, and (b) the timings of matching events in between the two corresponding traces do not differ by more than epsilon. We show that we can compute the bisimulation distance between two timed automata to within any desired degree of accuracy. We also show that the timed verification logic TCTL is robust with respect to our notion of quantitative bisimilarity, in particular, if a system satisfies a formula, then every close system satisfies a close formula.
Timed games are used for distinguishing between the actions of several agents, typically a controller and an environment. The controller must achieve its objective against all possible choices of the environment. The modeling of the passage of time leads to the presence of zeno executions, and corresponding unrealizable strategies of the controller which may achieve objectives by blocking time. We disallow such unreasonable strategies by restricting all agents to use only receptive strategies --- strategies which while not being required to ensure time divergence by any agent, are such that no agent is responsible for blocking time. Time divergence is guaranteed when all players use receptive strategies. We show that timed automaton games with receptive strategies can be solved by a reduction to finite state turn based game graphs. We define the logic timed alternating-time temporal logic for verification of timed automaton games and show that the logic can be model checked in EXPTIME. We also show that the minimum time required by an agent to reach a desired location, and the maximum time an agent can stay safe within a set of locations, against all possible actions of its adversaries are both computable.
We next study the memory requirements of winning strategies for timed automaton games. We prove that finite memory strategies suffice for safety objectives, and that winning strategies for reachability objectives may require infinite memory in general. We introduce randomized strategies in which an agent can propose a probabilistic distribution of moves and show that finite memory randomized strategies suffice for all omega-regular objectives. We also show that while randomization helps in simplifying winning strategies, and thus allows the construction of simpler controllers, it does not help a player in winning at more states, and thus does not allow the construction of more powerful controllers.
Finally we study robust winning strategies in timed games. In a physical system, a controller may propose an action together with a time delay, but the action cannot be assumed to be executed at the exact proposed time delay. We present robust strategies which incorporate such jitters and show that the set of states from which an agent can win robustly is computable.
Advisors: Pravin Varaiya and Thomas A. Henzinger
BibTeX citation:
@phdthesis{Prabhu:EECS-2008-97,
Author= {Prabhu, Vinayak},
Title= {Games for the Verification of Timed Systems},
School= {EECS Department, University of California, Berkeley},
Year= {2008},
Month= {Aug},
Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-97.html},
Number= {UCB/EECS-2008-97},
Abstract= {Models of timed systems must incorporate not only the sequence of system
events, but the timings
of these events as well to capture the real-time aspects of physical systems.
Timed automata are models of real-time systems in which states consist
of discrete locations and values for real-time clocks.
The presence of real-time clocks leads to an uncountable state space.
This thesis studies verification problems on timed automata in a game theoretic
framework.
For untimed systems, two systems are close if every
sequence of events of one system is also observable in the
second system.
For timed systems, the difference in timings of the two corresponding
sequences is also of importance.
We propose the notion of bisimulation distance which quantifies
timing differences; if the bisimulation distance between two systems is
epsilon, then (a) every
sequence of events of one system has a corresponding
matching sequence in the other, and
(b) the timings of matching events in between the
two corresponding traces do not differ by more than epsilon.
We show that we can compute the bisimulation distance between
two timed automata to within any desired degree of accuracy.
We also show that the timed verification logic TCTL is robust with respect to
our notion of quantitative bisimilarity,
in particular, if a system satisfies a
formula, then every close system satisfies a close formula.
Timed games are used for distinguishing between the actions of several agents,
typically a controller and an environment.
The controller must achieve its objective against all possible choices
of the environment.
The modeling of the passage of time leads to the presence of zeno
executions, and corresponding unrealizable strategies of the controller
which may achieve objectives by blocking time.
We disallow such unreasonable strategies by restricting all agents to use
only receptive strategies --- strategies which while not being required
to ensure time divergence by any agent, are such that no agent is responsible
for blocking time.
Time divergence is guaranteed when all players use receptive
strategies.
We show that timed automaton games with receptive strategies
can be solved by a
reduction to finite state turn based game graphs.
We define the logic timed alternating-time temporal logic for verification
of timed automaton games and show that the logic can be model checked in
EXPTIME.
We also show that the minimum time required by an agent to reach a desired
location, and the maximum time an agent can stay safe within a set
of locations, against all possible actions of its adversaries
are both computable.
We next study the memory requirements of winning strategies for timed
automaton games.
We prove that finite memory strategies suffice for safety objectives, and that
winning strategies for reachability objectives may require infinite memory
in general.
We introduce randomized strategies in which an agent can propose a
probabilistic distribution of moves and show that
finite memory randomized strategies suffice for all omega-regular
objectives.
We also show that while randomization helps in simplifying winning
strategies, and thus allows the construction of simpler controllers,
it does not help a player in winning at more states, and
thus does not allow the construction of more powerful controllers.
Finally we study robust winning strategies in timed games.
In a physical system, a controller may propose an action together with a time
delay, but the action cannot be assumed to be executed at the exact proposed
time delay.
We present robust strategies which incorporate such jitters and show that
the set of states from which an agent can win robustly is computable.},
}
EndNote citation:
%0 Thesis %A Prabhu, Vinayak %T Games for the Verification of Timed Systems %I EECS Department, University of California, Berkeley %D 2008 %8 August 15 %@ UCB/EECS-2008-97 %U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-97.html %F Prabhu:EECS-2008-97