List of Accepted Papers at FORMATS'08

Louis-Marie Traonouez, Didier Lime and Olivier H. Roux. Parametric model-checking of time Petri nets with stopwatches using the state-class graph
Abstract: In this paper, we propose a new framework for the parametric verification
of time Petri nets with stopwatches controlled by inhibitor arcs. We first
introduce an extension of time Petri nets with inhibitor arcs (ITPNs) with
temporal parameters.  Then, we define a symbolic representation of the
parametric state space based on the classical state class graph method. The
parameters of the model are embedded into the firing domains of the classes,
that are represented by convex polyhedra. Finally, we propose semi-algorithms
for the parametric model-checking of a subset of parametric TCTL formulae on
ITPNs.  We can thus generate the set of the parameter valuations that satisfy
the formulae.
Jasper Berendsen and Frits Vaandrager. Compositional Abstraction in Real-Time Model Checking
Abstract: The idea to use simulations (or refinements) as a compositional abstraction device is well-known, both in untimed and timed settings, and has already been studied theoretically and practically in many papers during the last three decades. Nevertheless, existing approaches do not handle two fundamental modeling concepts which, for instance, are frequently used in the popular Uppaal model checker: (1) a parallel composition operator that supports communication via shared variables as well as synchronization of actions, and (2) committed locations. In this paper, we describe a framework for compositional abstraction based on simulation relations that does support both concepts, and that is suitable for Uppaal. Our approach is very general and the only essential restriction is that the guards of input transitions do not depend on external variables. We have applied our compositional framework to verify the Zeroconf protocol for an arbitrary number of hosts.
Mani Chandy, Concetta Pilotto and Sayan Mitra. Convergence Verification: From Synchronous to Partially Synchronous  Systems
Abstract: Verification of partially synchronous distributed systems is difficult because of
inherent concurrency and the potentially large state space of the channels.
This paper identifies a subclass of such systems for which convergence properties can be verified based on the proof of convergence for the corresponding discrete-time shared state system. The proof technique extends to a class of partially synchronous systems in which an agent's state also evolves continuously over time. The proof techniques have been formalized in the PVS interface for timed I/O automata and applied to verify convergence of a mobile agent pattern formation algorithm.
Hanifa Boucheneb and Kamel Barkaoui. Relevant timed schedules / clock valuations for constructing time Petri net reachability graphs
Abstract: We consider here time Petri nets (the TPN model) and two of its
state space abstractions: the state class graph (SCG) and the zone
based graph (ZBG). We show that only some time points of the
clock/firing domains of abstract states are relevant to construct
a TPN reachability graph. Moreover, for the state class graph
method, the graph computed using relevant time points is smaller
than the SCG.
julien schmaltz and Jan Tretmans. On Conformance Testing for Timed Systems
Abstract: Conformance testing for labeled transition systems starts with
  defining when an implementation conforms to its specification.
  One of the formal theories for model-based testing uses
  the implementation relation $\ioco$ for this purpose.
  A peculiar aspect of $\ioco$ is to consider the absence of
  outputs as an observable action, named \emph{quiescence}.
  Recently a number of real-time extensions of ioco have been
  proposed in the literature.
  Quiescence and the observation of arbitrary delays are issues
  when defining such extensions.
  We present two new timed implementation relations and show their
  relation with existing ones.
  Based on these new definitions and using
  several examples, we show the subtle differences,
  and the consequences that small modifications in the definitions
  can have on the resulting relations.
  Moreover, we present conditions under which
  some of these implementation relations coincide.
  The notion of M-quiescence, i.e., if outputs occur in a system
  they occur before a delay M, turns out to be important
  in these conditions.
Michal Rutkowski, Marcin Jurdzinski, Ranko Lazic, Patricia Bouyer and Thomas Brihaye. Average-Price and Reachability-Price Games on Hybrid Automata with Strong Resets
Abstract: We introduce and study hybrid automata with strong resets.
  They generalize o-minimal hybrid automata, a class of hybrid automata
  which allows modeling of complex continuous dynamics.
  A number of analysis problems, such as reachability testing and
  controller synthesis, are decidable for classes of o-minimal hybrid
  We generalize existing decidability results for controller synthesis
  on hybrid automata and we establish new ones by proving that
  average-price and reachability-price games on hybrid automata with
  strong resets are decidable, provided that the structure on which
  the hybrid automaton is defined has a decidable first-order theory.
  Our proof techniques include a novel characterization of values in
  games on hybrid automata by optimality equations, and a definition of
  a new finitary equivalence relation on the states of a hybrid automaton
  which enables a reduction of games on hybrid automata to games on
  finite graphs.
Aldric Degorre and Oded Maler. On Scheduling Policies for Streams of Structured Jobs
Abstract: We study a class of scheduling problems which combines the
structural aspects associated with task dependencies, with the dynamic
aspects associated with ongoing streams of requests that arrive during
execution. For this class of problems we develop a scheduling policy
which can guarantee bounded accumulation of backlog for all admissible request streams. We show, nevertheless,
that no such policy can guarantee bounded latency for all request
Vijay Suman, Paritosh Pandya, Krishna S and Lakshmi Manasa G. Timed Automata with Integer Resets: Langauge Inclusion and Expressiveness
Abstract: In this paper, we consider a syntactic subset of timed
automata called  integer reset timed  automata (IRTA) where
{\em resets} are restricted to  occur at integral time points.
We argue with examples that the notion of global sparse time base used in
time triggered  architecture and distributed web  services can naturally be
modelled/specified as IRTA. As our main result, we show that the
language inclusion problem $L(A) \subseteq L(B)$ for a timed automaton
$A$ and an  IRTA $B$ is decidable with doubly exponential time
The expressive  power and the closure properties of IRTA are  also summarized.
In particular, the IRTA are (highly succinct but) expressively equivalent to
1-clock deterministic  IRTA and they  are closed under boolean operations.
Marcin Jurdzinski and Ashutosh Trivedi. Concavely priced timed automata
Abstract: Concavely priced timed automata, a generalisation of linearly priced
timed automata, are introduced.  Reachability-price and ratio-price
problems for the  concavely priced timed are considered
and they are proved to be PSPACE-complete.  This paper generalises the
recent work of Bouyer et al. on reachability-price and ratio-price
problems for linearly priced timed automata.
Joost-Pieter Katoen and Alexandru Mereacre. Verifying Inhomogeneous Markov Chains
Abstract: This paper presents a stochastic variant of Hennessy-Milner logic that is interpreted
over (state-labeled) inhomogeneous continuous-time Markov chains (ICTMCs), i.e.,
Markov chains in which transition rates are functions over time $t$. For piecewise constant rate functions, the model-checking problem is shown to be reducible to finding the zeros of an exponential polynomial. Using Sturm sequences and Newton's method, we obtain an approximative model-checking algorithm which is linear in the size of the ICTMC, logarithmic in the number of bits precision, and exponential in the nesting depth of the formula.
Carlo Alberto Furia and Matteo Rossi. MTL with Bounded Variability: Decidability and Complexity
Abstract: This paper investigates the properties of Metric Temporal Logic (MTL) over models in which time is dense but phenomena are constrained to have bounded variability. Contrary to the case of generic dense-time behaviors, MTL is proved to be fully decidable over models with bounded variability, if the variability bound is given. In these decidable cases, MTL complexity is shown to match that of simpler decidable logics such as MITL. On the contrary, MTL is undecidable if all behaviors with variability bounded by some generic constant are considered, but with an undecidability degree that is lower than in the case of generic behaviors.
Anne Remke and Boudewijn Haverkort. A uniformization-based algorithm for model checking CSL until operators on labelled queueing networks
Abstract: We present a model checking procedure for the CSL until operator on the CTMCs that underlie Jackson queueing networks. The key issue lies in the fact that the underlying CTMC is infinite in as many dimension as there are queues in the JQN. We need to compute the transient state probabilities for all goal states and for all possible starting states.  However, for the transient probabilities no results are readily available. We use an unifromization-based apporach to compute the transient state probabilities. Furthermore, we show how the highly structured state space of JQNs then allows us to compute the possible infinite satisfaction set for until formulas. A case study on an e-business site shows the feasibility of our approach.
Krishnendu Chatterjee, Thomas Henzinger and Vinayak Prabhu. Timed Parity Games: Complexity and Robustness
Abstract: We consider concurrent two player games played in real time on timed automaton game structures with parity objectives. To disallow zeno-runs, we restrict both players to use only receptive strategies, which while ensuring that no player is responsible for blocking time, do not require any player to guarantee time-divergence. First, we present an efficient reduction of these games to turn-based finite state parity games. Hence the rich class of algorithms for turn-based parity games can now be applied to timed automaton parity games. As a consequence of our reduction we also improve the complexity of timed automaton parity games.

Second, we consider two classes of robust strategies for the controller: namely, limit-robust and bounded-robust strategies. A limit-robust strategy of the controller must allow for some non-zero jitter in each of its moves.A bounded-robust strategy of the controller must allow for a jitter that is a known fixed constant for the system. We present efficient reduction to timed automaton games for solutions of both cases, and demonstrate that limit-robust strategies are strictly more powerful than bounded-robust strategies.
Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey and Jiri Srba. Infinite Runs in Weighted Timed Automata with Energy Constraints
Abstract: We study the problems of existence and construction of
infinite schedules for finite weighted automata and one-clock weighted
timed automata, subject to boundary constraints on the accumulated

More specifically, we consider automata equipped with positive and
negative weights on transitions and locations, corresponding to the
production and consumption of some resource (e.g. energy). We ask the
question whether there exists an infinite path for which the
accumulated weight for any finite prefix satisfies certain
constraints: for the lower-bound problem, we require the accumulated
weight never drop below zero, for the interval-bound problem it is to
stay within a given interval, and in the lower-weak-upper-bound
problem the accumulated weights may not drop below zero with the
additional feature that the weights never accumulate to more than a
given upper bound; any increases above this bound are simply
truncated. We also consider a game version of the above, where certain
transitions may be uncontrollable.

For finite weighted automata we show that the lower- and
lower-weak-upper-bound problems are decidable in polynomial time. This
remains true even in the game setting, where we also prove P-hardness
of the problem.  The interval-bound problem is on the other hand
NP-hard but decidable in PSPACE (at least), and in the game setting it
is EXPTIME-complete.

For one-clock weighted timed automata, the lower- and
lower-weak-upper-bound problems remain in P (also for the games), but the
interval-bound problem in the game setting is already undecidable.
Frits Vaandrager, Georgeta Igna, Venkatesh Kannan, Yang Yang, Twan Basten, Marc Geilen, Marc Voorhoeve, Sebastian De Smet and Lou Somers. Formal Modeling and Scheduling of Data Paths of Digital Document Printers
Abstract: We apply three different modeling frameworks --- timed automata (Uppaal),
colored Petri nets and synchronous data flow --- to model a challenging
industrial case study that involves an existing state-of-the-art
image processing pipeline.  Each of
the resulting models is used to derive schedules for 7 concurrent
jobs ("use cases") in the presence of limited resources (processing
units, memory, USB bandwidth,..).
The three models and corresponding analysis results are compared.
Frédéric Boniol, Hladik Pierre-Emmanuel and claire pagetti. A Framework for Distributing Real-Time Functions
Abstract: The design of critical embedded real-time systems requires high confidence in
the architecture and the implemented functionalities. Classically, such functions are
supported on a single monoprocessor, behavior of which is completely predictable, while
the execution is totally deterministic. With the growing complexity of systems, it
becomes quite unavoidable to implement these systems on distributed architectures.
Scaling from mono to multiprocessor raises several issues which we address in this paper:
we propose a simple executive model based on time triggered paradigm and an automated
approach to allocate real-time tasks based on constraint resolution techniques. We illustrate the method on an industrial case study.
Alexander Rabinovich. Complexity of  Metric Temporal logic   with Counting
Abstract: The temporal  logic with counting
modalities (TLC) is the extension  of  until-since temporal logic
by ``counting modalities" C_n(X) and
(n\in \nat); for each $n$ the modality
C_n(X) says that X will be true at least at n points in the
next unit of time

In this paper we investigate the complexity of the satisfiability
problem for TLC and show that the problem is PSPACE complete when
the index of C_n  is coded in unary, and EXPSPACE complete when
the index is coded in binary. We also show that the satisfiability
problem for the until-since temporal logic extended by Pnueli's
modalities is PSPACE complete.