salle A. Turing CE4
23 March 2016 - 14h00
Selected TACAS 2016 Papers: a joint Software Analysis and Tempo seminar
by Radu Iosif from Verimag
Abstract: Dogan Ulus: Online Timed Pattern Matching
Timed pattern matching consists in finding all segments of a densetime
Boolean signal that match a pattern defined by a timed regular expression.
This problem has been formulated and solved in [17] via an offline algorithm that takes the signal and expression as inputs and produces the set of all matches, represented as a finite union of two-dimensional zones. In this work we develop an online version of this approach where the input signal is presented incrementally and the matching is computed incrementally as well. Naturally, the concept of derivatives of regular expressions due to Brzozowski [6] can play a role in defining what remains to match after having read a prefix of the
signal. However the adaptation of this concept is not a straightforward for two
reasons: the dense infinite-state nature of timed behaviors and the fact that we are interested in matching, not only in prefix acceptance. To resolve these issues we develop an alternative theory of signals and expressions based on absolute time and show how derivatives are defined and computed in this setting. We then implement an online timed pattern matching algorithm based on these results.
--------------------------------------------------------------------------------
Radu Iosif: Abstraction Refinement for Trace Inclusion of Infinite State Systems
A emph{data automaton} is a finite automaton equipped with variables (counters or registers) ranging over infinite data domains. The transitions of the automaton are controlled by first-order formulae, encoding guards and updates. A trace of a data automaton is an alternating sequence of alphabet symbols and values taken by the counters during an execution of the automaton. The problem addressed
in this paper is the inclusion between the sets of traces (data languages) recognized by such automata. Since the problem is undecidable, we give a semi-algorithm based on abstraction refinement, which is proved to be sound and complete, but whose termination is not guaranteed. We have implemented our technique in a prototype tool and show promising results on several non-trivial examples. Joint work with Adam Rogalewicz and Tomas Vojnar (Brno, CZ)
