Parallel reachability analysis for hybrid systems

Amit Gurung, Arup Deka, Ezio Bartocci, Sergiy Bogomolov, Radu Grosu, Rajarshi Ray

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

13 Citations (Scopus)

Abstract

We propose two parallel state-space-exploration algorithms for hybrid automaton (HA), with the goal of enhancing performance on multi-core shared-memory systems. The first uses the parallel, breadth-first-search algorithm (PBFS) of the SPIN model checker, when traversing the discrete modes of the HA, and enhances it with a parallel exploration of the continuous states within each mode. We show that this simple-minded extension of PBFS does not provide the desired load balancing in many HA benchmarks. The second algorithm is a task-parallel BFS algorithm (TP-BFS), which uses a cheap precomputation of the cost associated with the post operations (both continuous and discrete) in order to improve load balancing. We illustrate the TP-BFS and the cost precomputation of the post operators on a support-function-based algorithm for state-space exploration. The performance comparison of the two algorithms shows that, in general, TP-BFS provides a better utilization/load-balancing of the CPU. Both algorithms are implemented in the model checker XSpeed. Our experiments show a maximum speed-up of more than 2000 χ on a navigation benchmark, with respect to SpaceEx LGG scenario. In order to make the comparison fair, we employed an equal number of post operations in both tools. To the best of our knowledge, this paper represents the first attempt to provide parallel, reachability-analysis algorithms for HA.

Original languageEnglish
Title of host publication2016 ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2016
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages12-22
Number of pages11
ISBN (Electronic)9781509027910
DOIs
Publication statusPublished - 27 Dec 2016
Externally publishedYes
Event14th ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2016 - Kanpur, India
Duration: 18 Nov 201620 Nov 2016

Publication series

Name2016 ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2016

Conference

Conference14th ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2016
Country/TerritoryIndia
CityKanpur
Period18/11/1620/11/16

Fingerprint

Dive into the research topics of 'Parallel reachability analysis for hybrid systems'. Together they form a unique fingerprint.

Cite this