TCS / Research / Publications / Checking Bounded Reachability in Asynchronous Systems by Symbolic Event Tracing
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

Checking Bounded Reachability in Asynchronous Systems by Symbolic Event Tracing

Reference:

Jori Dubrovin. Checking bounded reachability in asynchronous systems by symbolic event tracing. Technical Report TKK-ICS-R14, Helsinki University of Technology, Department of Information and Computer Science, Espoo, Finland, April 2009.

Abstract:

This report presents a new symbolic technique for checking reachability properties of asynchronous systems by reducing the problem to satisfiability in restrained difference logic. The analysis is bounded by fixing a finite set of potential events, each of which may occur at most once in any order. The events are specified using high-level Petri nets. The logic encoding describes the space of possible causal links between events rather than possible sequences of states as in Bounded Model Checking. Independence between events is exploited intrinsically without partial order reductions, and the handling of data is symbolic. On a family of benchmarks, the proposed approach is consistently faster than Bounded Model Checking. In addition, this report presents a compact encoding of the restrained subset of difference logic in propositional logic.

Keywords:

formal verification, Bounded Model Checking, partial order method, Coloured Petri Nets, difference logic

Suggested BibTeX entry:

@techreport{TKK-ICS-R14,
    address = {Espoo, Finland},
    author = {Jori Dubrovin},
    institution = {Helsinki University of Technology, Department of Information and Computer Science},
    month = {April},
    number = {TKK-ICS-R14},
    pages = {39},
    title = {Checking Bounded Reachability in Asynchronous Systems by Symbolic Event Tracing},
    type = {Technical Report},
    year = {2009},
}

PDF (432 kB)

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 19 January 2010.