The Computer Science Colloquium

Anatol Slissenko
(University Paris 12)

"Models of bounded complexity in describing decidable classes in predicate logic with time"

The problem under consideration is motivated by the verification of reactive distributed real-time systems. The time maybe discrete or continuous, time constraints may involve arithmetical operations and parameters (abstract constants), and, moreover, other parameters may be present e.g., the number of processes of distributed algorithm. The decidable classes are defined semantically in terms of two properties : finite refutability (that is relatively easy to check in concrete situations) and finite satisfiability (that is more difficult to check). The decidability algorithm, return for a given formula a quantifier free description of parameters for which the formula is false (true). The latter property is important for the verification as this quantifier free formula gives an exhaustive description of counter-examples that can be used to trace the errors. Experimental results and open theoretical problems will be also discussed.

The Colloquium is supported by generous contributions from the Bloomberg, Information Builders, Inc. and Netlogic, Inc.