TR03-04 (2003) – Incremental Counting Satisfiability for Real-Time Systems

S. Andrei, W.-N. Chin

Counting the number of truth assignments in a propositional formula has anumber of applications, including the verification of timing constraintsforreal-time specification. This number can tell us how “far away” is agivenspecification from satisfying its safety assertion. However,specificationsand safety assertions are often modified in an incremental fashion, whereproblematic bugs are fixed one at a time. To mirror such changes, wepropose an incremental algorithm for counting satisfiability. Ourproposedincremental algorithm is optimal as no unnecessary nodes are createdduring each incremental counting. To illustrate this application, we showhow incremental satisfiability counting can be applied to a well-knownrail-road crossing example, when its specification is being modified.

A concise and revised version of the paper was accepted at the10th IEEE Real-Time and Embedded Technology and Applications Symposium(RTAS 2004).

Bibtex

@TechReport{cav,
  author = "S. Andrei and  W.-N. Chin",
  title = "Incremental {C}ounting {S}atisfiability for {R}eal-{T}ime {S}ystems",
  institution = "``Al.I.Cuza'' University of Ia{c s}i, 
                 Faculty of Computer Science",
  year = "2003",
  number = "TR 03-04",
  note = "URL:http://www.infoiasi.ro/~tr/tr.pl.cgi"
}