CMU-CS-03-117
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-03-117

A Boolean Approach to Unbounded, Fully Symbolic
Model Checking of Timed Automata

Sanjit A. Seshia, Randal E. Bryant

March 2003

A shorter version of this apper will appear at CAV '03.

CMU-CS-03-117.ps
CMU-CS-03-117.pdf


Keywords: Timed automata, model checking, Boolean logic, separation logic, Quanti er elimination


We present a new approach to unbounded, fully symbolic model checking of timed automata that is based on an efficient translation of quantified separation logic to quantified Boolean logic. Our technique preserves the interpretation of clocks over the reals and can check any property expressed in the timed μ calculus. The core operations of eliminating quantifiers over real variables and deciding separation logic are respectively translated to eliminating quantifiers on Boolean variables and checking Boolean satisfiability (SAT). We can thus leverage well-known techniques for Boolean formulas, including Binary Decision Diagrams (BDDs) and recent advances in SAT and SAT-based quantifier elimination. We present preliminary empirical results for a BDD-based implementation of our method.

25 pages


Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu