Authors : Zine El Abidine Bounab and Salim Benayoune
Abstract: 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.
Zine El Abidine Bounab and Salim Benayoune, 2018. Model Checking Auto-Concurrency. Journal of Engineering and Applied Sciences, 13: 557-563.