scholarly journals Sequential and Parallel Algorithms for the State Space Exploration

2016 ◽  
Vol 16 (1) ◽  
pp. 3-18 ◽  
Author(s):  
Lamia Allal ◽  
Ghalem Belalem ◽  
Philippe Dhaussy ◽  
Ciprian Teodorov
Keyword(s):  
Model Checking ◽  
Parallel Algorithms ◽  
State Space ◽  
Parallel Algorithm ◽  
Space Exploration ◽  
The State ◽  
State Space Exploration

Abstract In this article, we are interested in the exploration part of model checking which consists in traversing all the possible states of a system. We propose two approaches to exploration, parallel and sequential. We present a comparison between our parallel approach and the parallel algorithm proposed in SPIN.

scholarly journals A Parallel Algorithm for the State Space Exploration

2016 ◽  
Vol 17 (2) ◽  
Author(s):  
Lamia Allal ◽  
Ghalem Belalem ◽  
Philippe Dhaussy ◽  
Ciprian Teodorov
Keyword(s):  
State Space ◽  
Parallel Algorithm ◽  
Space Exploration ◽  
The State ◽  
State Space Exploration

scholarly journals Efficient CSP Model Checking for Symbolic State-space Exploration with Application in Bacterial Chemo-Taxis Modelings

2020 ◽  
Author(s):  
Jing GUO
Keyword(s):  
Model Checking ◽  
State Space ◽  
Space Exploration ◽  
Bacterial Chemotaxis ◽  
The State ◽  
Decision Diagrams ◽  
Two Phases ◽  
Time Required ◽  
State Space Exploration ◽  
State Functions

Abstract Event locality is a class of theory that can clearly minimizes the memory and time required to store the state space. We present the multi-way decision diagrams to encode the next-state functions based on event locality and CSP’s stable failure. Instead of studying symbolic overall model, we apply the above thinking to the set of sub-models. Furthermore, we focus on saturation algorithms for CSP theory. And the algorithms consist of two phases, the universal process’s saturation checking and the single CSP symbol’s saturation checking. In the former case, the algorithms discuss better iteration strategy and recursive local fifix-point computations. In the latter case, the the single CSP symbol’s saturation checking calls the former algorithms, being combined preformed events and refusal events. Finally, we discuss bacterial chemotaxis modeled in CSP’s framework and saturation checking used to check the predefifined properties. The all algorithms are implemented in CSP tool FDR, the running results show that our algorithms often perform signifificantly faster than other conventional algorithms.

scholarly journals Probability, Parallelism and the State Space Exploration Problem

1998 ◽  
pp. 165-179 ◽  
Author(s):  
William Knottenbelt ◽  
Mark Mestern ◽  
Peter Harrison ◽  
Pieter Kritzinger
Keyword(s):  
State Space ◽  
Space Exploration ◽  
The State ◽  
State Space Exploration

scholarly journals Accurate Power Estimation for Sequential CMOS Circuits Using Graph-based Methods

VLSI Design ◽  
2001 ◽  
Vol 12 (2) ◽  
pp. 187-203
Author(s):  
Miriam Leeser ◽  
Valerie Ohm
Keyword(s):  
State Space ◽  
Space Exploration ◽  
Average Power ◽  
Power Estimation ◽  
The State ◽  
Estimation Methods ◽  
Cmos Circuits ◽  
State Transition Graph ◽  
Reconvergent Fanout ◽  
State Space Exploration

We present a novel method for estimating the power of sequential CMOS circuits. Symbolic probabilistic power estimation with an enumerated state space is used to estimate the average power switched by the circuit. This approach is more accurate than simulation based methods. Automatic circuit partitioning and state space exploration provide improvements in run-time and storage requirements over existing approaches. Circuits are automatically partitioned to improve the execution time and to allow larger circuits to be processed. Spatial correlation is dealt with by minimizing the cutset between partitions which tends to keep areas of reconvergent fanout in the same partition. Circuit partitions can be recombined using our combinational estimation methods which allow the exploitation of knowledge of probabilities of the circuit inputs. We enumerate the state transition graph (STG) incrementally using state space exploration methods developed for formal verification. Portions of the STG are generated on an as-needed basis, and thrown away after they are processed. BDDs are used to compactly represent similar states. This saves significant space in the storage of the STG. Our results show that modeling the state space is imperative for accurate power estimation of sequential circuits, partitioning saves time, and incremental state space exploration saves storage space. This allows us to process larger circuits than would otherwise be possible

Sign in / Sign up

Export Citation Format

Share Document