Maximality-based symbolic model checking

Summary form only given. We deal with concurrent systems formal verification. On one hand, we consider maximality-based labeled transition system model (MLTS) which supports the maximality semantics. From this point of view we can omit action temporal and structural atomicity hypotheses; consequently, we can inherit results of combinatorial state space explosion problem solution based on the use of true concurrency semantics. On the other hand, MLTS structures are coded in term of binary decision diagrams (BDD). On these new structures we define and realize a symbolic model checking algorithm for which the verified properties are written in CTL logic.