A planning model for concurrent Asyncronus Automata

In this work a new approach based on planning paradigm is proposed in order to describe the interactions of concurrent asynchronous automata. The behaviour of a set of nondeterministic asynchronous automata which interact via common variables in a conflictfree environment is modelled through an appropriate planning domain such that the set of valid plans in the domain represents the set of possible behaviours of the concurrent automata system. The consequence of the method is that verifying and checking properties of the automata system can be seen as solving appropriate planning problems with additional constraints on solution plans, such as temporally extended goals. The proposed model allows a straightforward description of automata in a portable and planner independent way, thus recent advancements in plan synthesis algorithms can be applied and exploited as well. The validity of the approach has been experimentally verified on recent planners in order to check properties of classical examples of protocols in an automata community such as deadlock and states reachability. The approach represents in some sense the counterpart of recent proposals based on planning via model checking. The presented technique for modelling concurrent automata by planning allows to extend the applicability of planners not only to model checking but also to problems of behaviours coordination, and plan synthesis with a plurality of actors