Luboš Brim and Mojmír Křetinský:
Model-Checking Large Finite State Systems and Beyond

In the talk we give an overview of recent developments in the area of model-checking very large finite state systems and infinite state systems.

Despite significant advances in the model-checking technology its applicability to extremely large or even infinite state systems is still limited. A possible approach to dealing with large finite state systems is to increase the computational power (especially memory) by building a powerful parallel computer as a network of workstations in which individual workstations communicate via a message passing interface. We highlight the techniques and methods used in distributed analysis and verification of large systems on a particular case of LTL model-checking. We survey most of the known distributed enumerative LTL model checking algorithms, compare them both theoretically and experimentally, discuss their advantages and disadvantages, and determine cases in which individual algorithms are more appropriate than the others.

Automatic verification of current software systems often needs to model them as infinite-state systems, i.e. systems with an evolving structure and/or operating on unbounded data types. Infinite-state systems can be specified in a number of ways with their respective advantages and limitations. Petri nets, pushdown automata, and process algebras like BPA, BPP, or PA all serve to exemplify this. Here we employ the classes of infinite-state systems defined by term rewrite systems and called Process Rewrite Systems (PRS) as introduced by Mayr. PRS subsume a variety of the formalisms studied in the context of formal verification (e.g. all the models mentioned above). We present a hierarchy of PRS (sub)classes; their relevance for modelling and analysing programs is briefly mentioned. Also, we explore the model checking problem over these classes with respect to various linear- and branching-time logics.