Auditorium (Building IMAG)
27 janvier 2020 - 14h00
Thesis Defence - Xiao XU - Generalisation of Alternating Automata over Infinite Alphabets (Phd Defense)
par Xiao XU de VERIMAG
Abstract: The language inclusion problem is recognised as being central to verification in different domains, such as hardware, communication protocols, software systems, etc. There we might face two challenges: non-determinism and infinite alphabets.
We propose two models of alternating automata over infinite alphabets: (i) alternating data automata (ADA) and (ii) first-order alternating data automata (FOADA). They both recognise the data words over infinite alphabets. In ADA model, the control states are Booleans and the transition rules are specified by a set of formulae in a combined first-order theory of states (Booleans) and data that relate past values of variables with current values of variables. But a restriction of the ADA model is that, there is not hidden variable, hence all the data values taken by the variables are visible in the input. But in FOADA model, the arguments of a predicate atom track the values of the internal variables associated with the state, and these values are invisible in the input sequence, which overcomes the restriction of the ADA model.
With these two alternating models, Boolean operations of union, intersection and complement can be done in linear time, thus matching the complexity of performing these operations in the finite-alphabet case. However, the price to be paid here is that the emptiness checking becomes undecidable. For this reason, we provide two efficient semi-algorithms for emptiness checking: (i) lazy predicate abstraction and (ii) IMPACT method. These semi-algorithms are proven to terminate by returning a word from the language of the given automaton if one exists; but if the language of the given automaton is empty, then the termination is not guaranteed.
The main application of our models is checking inclusions between various classes of automata extended with variables ranging over infinite domains that recognise languages over infinite alphabets. The most widely known classes of this kind are timed automata and finite-memory (register) automata. Another application is checking safety (mutual exclusion, absence of deadlocks, etc.) and liveness (termination, lack of starvation, etc.) properties of parameterised concurrent programs.
Besides the theoretical parts, we also have developed a tool - FOADA Checker, mainly used for checking inclusion between two automata or checking emptiness of an automaton. FOADA Checker is written in Java, via Java-SMT interface and using Z3 SMT solver for spuriousness, coverage queries and interpolant generation. The IMPACT semi-algorithm has been implemented in the tool to check the emptiness of an automaton.
