Feb 11, 2014: Andreas E. Dalsgaard: Distributed timed automata model checking using RDMA

February 11, 2014Distributed timed automata model checking using RDMA
Room: HalB 2FAndreas E. Dalsgaard

For timed automata model checking the state space is uncountably infinite, and therefore model checking have to be done on symbolic states, that make up a finite representation of the state space. Symbolic states may subsume smaller symbolic states and thereby substantially reduce the number of states that have to be explored. For parallel timed automata model checking it becomes essential to share big symbolic states with other workers before a large amount of smaller symbolic states and successors of these are explored. Previously, we extended the multi-core version of LTSmin with support for timed automata model checking and demonstrated good scalability by reusing the efficient lockless data structures implemented in LTSmin. For the distributed setting the challenge of timely sharing of big symbolic states with other workers become even harder. In this talk I will describe challenges and considerations faced from using remote direct memory access (RDMA) for timed automata model checking.