TY  - JOUR
T1  - Model Checking Auto-Concurrency
AU - El Abidine Bounab, Zine AU - Benayoune, Salim 
JO  - Journal of Engineering and Applied Sciences
VL  - 13
IS  - 3
SP  - 557
EP  - 563
PY  - 2018
DA  - 2001/08/19
SN  - 1816-949x
DO  - jeasci.2018.557.563
UR  - https://makhillpublications.co/view-article.php?doi=jeasci.2018.557.563
KW  - True concurrency semantics
KW  -process algebra
KW  -model checking
KW  -CTL
KW  -execution
KW  -transitions
AB  - This study defines a new operational semantics for a subset of CSP dedicated to express
concurrency. We have defined formally the translation from a specifications expressed in CSP to a true
concurrency semantic model called CLTS (Concurrent Labeled Transition System). CLTS is the unification of
two semantic model the multi-set labeled transition system where transition are labeled with a set of actions
instead of a single action and causality semantics where the dependences between actions is considered. The
main contribution of this research is to demonstrate that the algorithms for model checking suggested in the
literature which are based upon the interleaving semantics can be customized easily to the true concurrency
semantics for the verification of the new type of properties associated with the simultaneous execution of
actions in various transitions.
ER  -