Accession Number:

ADA460035

Title:

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

Descriptive Note:

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

2003-03-01

Pagination or Media Count:

26.0

Abstract:

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 mu 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.

Subject Categories:

  • Theoretical Mathematics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE