Model Checking MASL Specification of Distributed Real-Time Systems

We present model checking algorithms for MASL specification of distributed real-time systems. The proposed algorithms use symbolic model checking approach by analogy with model checking algorithms for branching-time temporal logic CTL and alternating-time temporal logic ATL. For the fixed environment case, the algorithm is polynomial-time in the specification length and sizes of the sets of system states and actions. For the dynamic environment case, the algorithm is polynomial-time in the model size, but it is exponential-time in the structure of environment specification.