scholarly journals Model-Checking Games for Fixpoint Logics with Partial Order Models

2009 ◽  
pp. 354-368 ◽  
Author(s):  
Julian Gutierrez ◽  
Julian Bradfield
Keyword(s):  
Model Checking ◽  
Partial Order

Partial-Order Reduction for GPU Model Checking

2016 ◽  
pp. 357-374 ◽  
Author(s):  
Thomas Neele ◽  
Anton Wijs ◽  
Dragan Bošnački ◽  
Jaco van de Pol
Keyword(s):  
Model Checking ◽  
Partial Order ◽  
Order Reduction ◽  
Partial Order Reduction

TEMPORAL LOGICS FOR TRACE SYSTEMS: ON AUTOMATED VERIFICATION

1993 ◽  
Vol 04 (01) ◽  
pp. 31-67 ◽  
Author(s):  
WOJCIECH PENCZEK
Keyword(s):  
Model Checking ◽  
Partial Order ◽  
Whole Language ◽  
Concurrent Systems ◽  
Parallel Execution ◽  
Automated Verification ◽  
Temporal Logics ◽  
Time Model ◽  
Exponential Time ◽  
Computation Tree

We investigate an extension of CTL (Computation Tree Logic) by past modalities, called CTL P, interpreted over Mazurkiewicz’s trace systems. The logic is powerful enough to express most of the partial order properties of distributed systems like serializability of database transactions, snapshots, parallel execution of program segments, or inevitability under concurrency fairness assumption. We show that the model checking problem for the logic is NP-hard, even if past modalities cannot be nested. Then, we give a one exponential time model checking algorithm for the logic without nested past modalities. We show that all the interesting partial order properties can be model checked using our algorithm. Next, we show that is is possible to extend the model checking algorithm to cover the whole language and its extension to [Formula: see text]. Finally, we prove that the logic is undecidable and we discuss consequences of our results on using propositional versions of partial order temporal logics to synthesis of concurrent systems from their specifications.

scholarly journals A Partial Order Approach to Branching Time Logic Model Checking

1999 ◽  
Vol 150 (2) ◽  
pp. 132-152 ◽  
Author(s):  
Rob Gerth ◽  
Ruurd Kuiper ◽  
Doron Peled ◽  
Wojciech Penczek
Keyword(s):  
Model Checking ◽  
Partial Order ◽  
Logic Model ◽  
Branching Time ◽  
Time Logic ◽  
Logic Model Checking

scholarly journals On the complexity of partial order trace model checking

2008 ◽  
Vol 106 (3) ◽  
pp. 120-126 ◽  
Author(s):  
Thierry Massart ◽  
Cédric Meuter ◽  
Laurent Van Begin
Keyword(s):  
Model Checking ◽  
Partial Order ◽  
Trace Model
Sign in / Sign up

Export Citation Format

Share Document