 Lorenzo Clemente,
Frédéric Herbreteau, Grégoire Sutre and Amélie Stainer.
Reachability of Communicating Timed Processes.
In proceedings of the 16th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'13), Rome, Italy, March 2013. Springer.
Abstract

Pdf
We study the reachability problem
for communicating timed processes, both in discrete and dense time. Our model comprises automata
with local timing constraints communicating over unbounded FIFO channels. Each automaton can only
access its set of local clocks; all clocks evolve at the same rate. Our main contribution is a
complete characterization of decidable and undecidable communication topologies, for both discrete
and dense time. We also obtain complexity results, by showing that communicating timed processes
are at least as hard as Petri nets; in the discrete time, we also show equivalence with Petri nets.
Our results follow from mutual topologypreserving reductions between timed automata and (untimed)
counter automata. To account for urgency of receptions, we also investigate the case where processes
can test emptiness of channels.

Amélie Stainer.
Frequencies in Forgetful Timed Automata.
In proceedings of the 10th International Conference on Formal Modeling and Analysis
of Timed Systems (Formats'12), London, UK, September 2012. Springer.
Abstract

Pdf
A quantitative semantics for infinite timed words in timed automata based on the frequency of a run is introduced in [BBBS11].
Unfortunately, most of the results are obtained only for oneclock timed automata because the techniques do not allow to deal with some phenomenon of convergence between clocks.
On the other hand, the notion of forgetful cycle is introduced in [BA11], in the context of entropy of timed languages, and seems to detect exactly these convergences.
In this paper, we investigate how the notion of forgetfulness can help
to extend the computation of the set of frequencies to nclock timed automata.
 Peter E. Bulychev,
Alexandre David,
Kim Guldstrand Larsen,
Axel Legay,
Guangyuan Li,
Danny Bogsted Poulsen and
Amélie Stainer
MonitorBased Statistical Model Checking for Weighted Metric
Temporal Logic.
In proceedings of the 18th International Conference on
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'12),
Mérida, Venezuela, March 2012. Springer.
Abstract

Pdf
We present a novel approach
and implementation for analysing weighted timed automata (WTA) with respect to
the weighted metric temporal logic (WMTL). Based on a stochastic semantics
of WTAs, we apply statistical model checking (SMC) to estimate and test
probabilities of satisfaction with desired levels of confidence. Our approach
consists in generation of deterministic monitors for formulas in
WMTL,
allowing for efficient SMC by runtime evaluation of a given formula. By
necessity, the deterministic observers are in general approximate (over or
underapproximations), but are most often exact and experimentally tight.
The technique is implemented in the new tool CASAAL. that we seamlessly
connect to UPPAALSMC. in a tool chain. We demonstrate the applicability
of our technique and the efficiency of
our implementation through a number of casestudies.
 Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye and Amélie Stainer.
Emptiness and Universality Problems in Timed Automata with Positive Frequency.
In proceedings of the 38th International Colloquium on Automata, Languages and Programming (ICALP'11), Zürich, Switzerland, July 2011. Springer.
Abstract

Pdf
The languages of infinite timed words
accepted by timed automata are traditionally defined using Büchilike conditions. These
acceptance conditions focus on the set of locations visited infinitely often along a run, but
completely ignore quantitative timing aspects. In this paper we propose a natural quantitative
semantics for timed automata based on the socalled frequency, which measures the proportion of
time spent in the accepting states. We study various properties of timed languages accepted
with positive frequency, and in particular the emptiness and universality problems.
 Nathalie Bertrand, Thierry Jéron, Amélie Stainer and Moez Krichen.
Offline Test Selection with Test Purposes for NonDeterministic Timed Automata.
In proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11), Saarbrücken, Germany, MarchApril 2011. Springer.
Abstract

Pdf
This paper proposes
novel offline test generation techniques for nondeterministic timed automata
with inputs and outputs (TAIOs) in the formal framework of the tioco conformance
theory. In this context, a first problem is the determinization of TAIOs, which
is necessary to foresee next enabled actions, but is in general impossible.
This problem is solved here thanks to an approximate determinization using a
game approach, which preserves tioco and guarantees the soundness of generated
test cases. A second problem is test selection for which a precise description
of timed behaviors to be tested is carried out by expressive test purposes modelled by a generalization of TAIOs.
Finally, using a symbolic coreachability analysis guided by the test purpose, test cases are generated in the form
of TAIOs equipped with verdicts.
 Nathalie Bertrand, Amélie Stainer, Thierry Jéron and Moez Krichen.
A game approach to determinize timed automata.
In proceedings of the 14th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'11), Saarbrücken, Germany, MarchApril 2011. Springer.
Abstract

Pdf
Timed automata are frequently used to model realtime
systems. Their determinization is a key issue for several validation
problems. However, not all timed automata can be determinized, and
moreover determinizability is undecidable. In this paper, we propose
a gamebased algorithm which, given a timed automaton, tries to produce a
languageequivalent deterministic timed automaton,
otherwise a deterministic overapproximation. Our method subsumes
two recent contributions: it is at once more general than the
determinization procedure of Baier et al [BBBBicalp09] and more precise
than the approximation algorithm of Krichen and Tripakis [KTfmsd09].