Fair Cycle Detection using Description Logic Reasoning.pdfVIP

Fair Cycle Detection using Description Logic Reasoning 1 1 1 2 Shoham Ben-David , Jeffrey Pound , Richard Trefler , Dmitry Tsarkov , Grant Weddell1 1. David R. Cheriton School of Computer Science, University of Waterloo 2. School of Computer Science, University of Manchester 1 Introduction Model checking ([12, 20], c.f.[11]) is a technique for verifying finite-state systems, that has been proven to be very effective in the verification of hardware and software pro- grams. In model checking, a model M , given as a set of state variables V and their next-state relations, is verified against a temporal logic formula ϕ. When ϕ holds on all computation paths of M we write M |= ϕ. The most commonly used temporal logics are Linear Temporal Logic (LTL) [19] and Computation Tree Logic (CTL) [12]. Temporal logic specifications, whether given in LTL or in CTL, are roughly divided into two basic categories [16, 1]: formulas that specify safety properties and formulas that specify liveness properties. Informally, a safety formula states that “something bad never happens”, and a violation of it can be shown by a finite prefix of a computation path, reaching a bad state. A liveness formula asserts that “something good will even- tually happen”, and a counterexample for it must contain an infinite path where a good state never appears (a cycle, in case of a finite model). A simple example of a liveness property is the CTL formula AFp asserting that the proposition p must appear even- tually on every computation path of the model. In many cases, a liveness formula ϕ is accompanied by a set of fairness constraints : Boolean events that must appear infi- nitely often on a path to make it fair . When fairness constraints are present, ϕ should only be verified on fair paths, and a counterexample sh