@article{MAKHILLJEAS201813315509,
    title = {Model Checking Auto-Concurrency},
    journal = {Journal of Engineering and Applied Sciences},
    volume = {13},
    number = {3},
    pages = {557-563},
    year = {2018},
    issn = {1816-949x},
    doi = {jeasci.2018.557.563},
    url = {https://makhillpublications.co/view-article.php?issn=1816-949x&doi=jeasci.2018.557.563},
    author = {Zine and},
    keywords = {True concurrency semantics,process algebra,model checking,CTL,execution,transitions},
    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.}
    }