Title: HORNSAT: A Uniform Approach to the Verification of Finite State
Branching Time Systems


Formal Verification of Finite State systems has been solved in many
different ways, such as automated theorem proving (e.g., PVS, Maude),
explicit state model checking (e.g., SPIN, Murphi), symbolic model
checking (e.g., SMV), Satisfiability based bounded Model Checking
(e.g. BMC) etc.

Depending on the kind of properties one cares to prove about a finite
state system, one might resort to logics of different expressive
powers. One major differentiation between such logics has been the
model of timing structure, namely linear time vs. branching
time. Whereas these two timing structures are provably of incomparable
expressive power, often times, one is preferred over the other based
not only on the expressive power, but also on the computational
complexity of verifying properties expressed in those logics.  For
finite state systems where state transitions are explicit, branching
time logics have considerably better time complexity, often linear
time in the size of the state space of the system. It turns out that
there are many different modeling approaches as well notions of
verifiability. For example, in model checking approach, a system is
modeled with finite state Kripke structures, and verifiability means
satisfaction of a logical formula in those structures. In process
algebraic approaches, systems are modeled with process algebras, and
the notion of verifiability is in establishing a process pre-order or
equivalence (e.g. simulation pre-order, bisimulation equivalence)
etc. These may seem quite different, but in this talk we show that all
such branching time relations and equivalences, as well as model
checking are very efficiently reducible to the problem of
satisfiability of Horn Clauses (a.k.a HORNSAT). The advantage of this
unifying view is many folds: (1) HORNSAT is a special class of SAT
problems that are solvable in polynomial time (in fact linear time);
(2) HORNSAT can be solved incrementally and on-the fly; and (3)
HORNSAT has efficient data structures which can be manipulated to
generate counter examples.

-----------------------------------------------------
Dr. Sandeep K. Shukla
Professor
Department of Computer Science and Engineering Indian Institute of
Technology, Kanpur Kanpur, India
http://www.cse.iitk.ac.in/users/sandeeps/