Formal verification of infinite-state systems is a rapidly growing area of research, with potential and actual applications to real-time and embedded systems, telecommunication protocols, infinite and unbounded data and control structures (counters, queues, etc.) parametrized systems (networks of arbitrary number of processes), etc.
Symbolic model checking is a methodology for formal verification, based on symbolic representation of states and transitions in models of systems which are to be verified, and on effective symbolic computation of the sets of states satisfying the properties of importance, such as pre- and post-conditions, reachability, safety, liveness, fairness, etc. Symbolic model checking is particularly essential in the case of infinite-state systems, which are not amenable to direct presentation and manipulation.
In this talk I will duscuss briefly the general topic of formal verification of infinite-state systems, and then will present some recent work (joint with my master student Wilmari Bekker, UJ) where infinite-state transition systems are modelled as rational graphs, with states labelled by the words in some regular language and transitions recognised by rational transducers (multi-head asynchronous finite automata), for which we have established an algorithmic method for symbolic model checking of local properties (pre-conditions and post-conditions), specified in the basic tense logic and some hybrid extensions of it.
Valentin Goranko is an associate professor at the School of Mathematics of the University of the Witwatersrand, Johannesburg. We completed his PhD in mathematical logic at the University of Sofia, Bulgaria, in 1988 and has 25 years of academic teaching experience in mathematics and computer science. His current research interests are mainly focused on theory and applications of logic to computer science and artificial intelligence.