- 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 topology-preserving 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 one-clock 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 n-clock timed automata.
- Peter E. Bulychev,
Alexandre David,
Kim Guldstrand Larsen,
Axel Legay,
Guangyuan Li,
Danny Bogsted Poulsen and
Amélie Stainer
Monitor-Based 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 run-time evaluation of a given formula. By
necessity, the deterministic observers are in general approximate (over- or
under-approximations), but are most often exact and experimentally tight.
The technique is implemented in the new tool CASAAL. that we seamlessly
connect to UPPAAL-SMC. in a tool chain. We demonstrate the applicability
of our technique and the efficiency of
our implementation through a number of case-studies.
- 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üchi-like 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 so-called 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.
Off-line Test Selection with Test Purposes for Non-Deterministic 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, March-April 2011. Springer.
Abstract
|
Pdf
This paper proposes
novel off-line test generation techniques for non-deterministic 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, March-April 2011. Springer.
Abstract
|
Pdf
Timed automata are frequently used to model real-time
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 game-based algorithm which, given a timed automaton, tries to produce a
language-equivalent deterministic timed automaton,
otherwise a deterministic over-approximation. Our method subsumes
two recent contributions: it is at once more general than the
determinization procedure of Baier et al [BBBB-icalp09] and more precise
than the approximation algorithm of Krichen and Tripakis [KT-fmsd09].