Activities per year
Abstract
Model checking is an automated verification procedure, which checks that a model of a system satisfies certain properties. These properties are typically expressed in some temporal logic, like LTL and CTL. Algorithms for LTL model checking (linear time logic) are based on automata theory and graph algorithms, while algorithms for CTL (computation tree logic) are based on fixedpoint computations and set operations.
The basic model checking procedures examine the state space of a system exhaustively, which grows exponentially in the number of variables or parallel components. Scalability of model checking is achieved by clever abstractions (for instance counterexample guided abstraction refinement), clever algorithms (for instance partialorder reduction), clever datastructures (for instance binary decision diagrams) and, finally, clever use of hardware resources, for instance algorithms for distributed and multicore computers.
This invited lecture will provide a number of highlights of our research in the last decade on highperformance model checking, as it is implemented in the open source LTSmin tool set, focusing on the algorithms and datastructures in its multicore tools.
A lockfree, scalable hashtable maintains a globally shared set of already visited state vectors. Using this, parallel workers can semiindependently explore different parts of the state space, still ensuring that every state will be explored exactly once. Our implementation proved to scale linearly on tens of processors.
Parallel algorithms for NDFS. Nested DepthFirst Search is a lineartime algorithm to detect accepting cycles in Büchi automata. LTL model checking can be reduced to the emptiness problem of Büchi automata, i.e. the absence of accepting cycles. We introduced a parallel version of this algorithm, despite the fact that DepthFirst Search is hard to parallelize. Our multicore implementation is compatible with important state space reduction techniques, in particular state compression and partialorder reduction and generalizes to timed automata.
A multicore library for Decision Diagrams, called Sylvan. Binary Decision Diagrams (BDD) have been introduced as concise representations of sets of Boolean vectors. The CTL model checking operations can be expressed directly on the BDD representation. Sylvan provides a parallel implementation of BDD operations for sharedmemory, multicore processors. We also provided successful experiments on distributed BDDs over a cluster of multicore computer servers. Besides BDDs, Sylvan also supports Multiway and Multiterminal Decision Diagrams.
Multicore algorithms to detect Strongly Connected Components. An alternative modelchecking algorithm is based on the decomposition and analysis of Strongly Connected Components (SCCs). We have implemented a parallel version of Dijkstra’s SCC algorithm. It forms the basis of model checking LTL using generalized Büchi and Rabin automata. SCCs are also useful for model checking with fairness, probabilistic model checking, and implementing partialorder reduction.
The basic model checking procedures examine the state space of a system exhaustively, which grows exponentially in the number of variables or parallel components. Scalability of model checking is achieved by clever abstractions (for instance counterexample guided abstraction refinement), clever algorithms (for instance partialorder reduction), clever datastructures (for instance binary decision diagrams) and, finally, clever use of hardware resources, for instance algorithms for distributed and multicore computers.
This invited lecture will provide a number of highlights of our research in the last decade on highperformance model checking, as it is implemented in the open source LTSmin tool set, focusing on the algorithms and datastructures in its multicore tools.
A lockfree, scalable hashtable maintains a globally shared set of already visited state vectors. Using this, parallel workers can semiindependently explore different parts of the state space, still ensuring that every state will be explored exactly once. Our implementation proved to scale linearly on tens of processors.
Parallel algorithms for NDFS. Nested DepthFirst Search is a lineartime algorithm to detect accepting cycles in Büchi automata. LTL model checking can be reduced to the emptiness problem of Büchi automata, i.e. the absence of accepting cycles. We introduced a parallel version of this algorithm, despite the fact that DepthFirst Search is hard to parallelize. Our multicore implementation is compatible with important state space reduction techniques, in particular state compression and partialorder reduction and generalizes to timed automata.
A multicore library for Decision Diagrams, called Sylvan. Binary Decision Diagrams (BDD) have been introduced as concise representations of sets of Boolean vectors. The CTL model checking operations can be expressed directly on the BDD representation. Sylvan provides a parallel implementation of BDD operations for sharedmemory, multicore processors. We also provided successful experiments on distributed BDDs over a cluster of multicore computer servers. Besides BDDs, Sylvan also supports Multiway and Multiterminal Decision Diagrams.
Multicore algorithms to detect Strongly Connected Components. An alternative modelchecking algorithm is based on the decomposition and analysis of Strongly Connected Components (SCCs). We have implemented a parallel version of Dijkstra’s SCC algorithm. It forms the basis of model checking LTL using generalized Büchi and Rabin automata. SCCs are also useful for model checking with fairness, probabilistic model checking, and implementing partialorder reduction.
Original language  English 

Title of host publication  Topics in Theoretical Computer Science 
Subtitle of host publication  Second IFIP WG 1.8 International Conference, TTCS 2017, Tehran, Iran, September 1214, 2017, Proceedings 
Editors  Mohammad Reza Mousavi, Jiri Sgall 
Publisher  Springer 
Pages  xvxvi 
Number of pages  2 
ISBN (Electronic)  9783319689531 
ISBN (Print)  9783319689524 
Publication status  Published  Nov 2017 
Event  Second IFIP WG 1.8 International Conference on Topics in Theoretical Computer Science, TTCS 2017  Institute for Research in Fundamental Sciences (IPM), Tehran, Iran, Islamic Republic of Duration: 12 Sep 2017 → 14 Sep 2017 Conference number: 2 http://ttcs.ir 
Publication series
Name  Lecture Notes in Computer Science 

Publisher  Springer 
Volume  10608 
ISSN (Print)  03029743 
ISSN (Electronic)  16113349 
Conference
Conference  Second IFIP WG 1.8 International Conference on Topics in Theoretical Computer Science, TTCS 2017 

Abbreviated title  TTCS 
Country/Territory  Iran, Islamic Republic of 
City  Tehran 
Period  12/09/17 → 14/09/17 
Internet address 
Keywords
 parallel model checking
 decision diagrams
 nested depthfirst search
 rabin automata
 strongly connected components
 lockfree hashtables
Fingerprint
Dive into the research topics of 'Parallel Algorithms for Model Checking'. Together they form a unique fingerprint.Activities
 1 Invited talk

Parallel Algorithms for Model Checking
Jaco van de Pol (Speaker)
12 Sep 2017Activity: Talk or presentation › Invited talk