A planning model for concurrent Asyncronus Automata

In this work a new approach based on planning paradigm isproposed in order to describe the interactions of concurrentasynchronous automata.The behaviour of a set of nondeterministic asynchronousautomata which interact via common variables in a conflictfree environment is modelled through an appropriateplanning domain such that the set of valid plans in thedomain represents the set of possible behaviours of theconcurrent automata system. The consequence of themethod is that verifying and checking properties of theautomata system can be seen as solving appropriateplanning problems with additional constraints on solutionplans, such as temporally extended goals.The proposed model allows a straightforward description ofautomata in a portable and planner independent way, thusrecent advancements in plan synthesis algorithms can beapplied and exploited as well.The validity of the approach has been experimentallyverified on recent planners in order to check properties ofclassical examples of protocols in an automata communitysuch as deadlock and states reachability.The approach represents in some sense the counterpart ofrecent proposals based on planning via model checking.The presented technique for modelling concurrent automataby planning allows to extend the applicability of plannersnot only to model checking but also to problems ofbehaviours coordination, and plan synthesis with a pluralityof actors