A Finite Representation of Durational Action Timed Automata Semantics

Durational action timed automata (daTAs) are state transition systems like timed automata (TAs) that capture information regarding the concurrent execution of actions and their durations using maximality-based semantics. As the underlying semantics of daTAs are infinite due to the modeling of time progress, conventional model checking techniques become impractical for systems specified using daTAs. Therefore, a finite abstract representation of daTA behavior is required to enable model checking for such system specifications. For that, we propose a finite abstraction of the underlying semantics of a daTA-like region abstraction of timed automata. In addition, we highlight the unique benefits of daTAs by illustrating that they enable the verification of properties concerning concurrency and action duration that cannot be verified using the traditional TA model. We demonstrate mathematically that the number of states in durational action timed automata becomes significantly smaller than the number of states in timed automata as the number of actions increases, confirming the efficiency of daTAs in modeling behavior with action durations.