by Laurent Fribourg

Abstract: In order to model concurrent systems whose resources (channels,
messages, clocks, parameters,...)

may take an illimited number of values, it is natural to consider extended
forms of finite-state automata.

Two main methods emerged these latter years for analysing such infinite-state
models. The first method, called ``symbolic model-checking'', defined suitable
classes of extended automata (timed automata, hybrid systems,...) and developed
specific analysis tools (HyTech, Kronos, Uppaal, Polka,...). The second
method, called ``deductive-algorithmic method'', consists in integrating
decision procedures, based on finite-state model-checking, into general
theorems provers (PVS, SteP, ...).

On the other hand, pursuing the same goal of infinite-state systems verification, several researchers recently explored the use of tools originating from logic programming with constraints (XSB, CLP(R), 2lp, Datalog with gap-constraints,...). In this tutorial, I will compare such a logic-programming based approach to the symbolic model-checking and deductive-algorithmic methods, by considering concrete examples of industrial protocol telecommunications. I will try to point out the merits and shortcomings of logic programming methods, and indicate some prospects.