A Reference Net Based Formalization of Concurrent Cognitive Decision Making

Multi-agent systems are said to possess considerable strengths like robustness, flexibility, and reliability. But their application in safety- and/or security-critical domains is often not accepted. This is because in such domains the correctness and predictability of a system must be validated by application of a huge amount of test sets or, in the worst case, verified by formal methods. However, verifying multi-agent systems can be very complex or even impossible. Note that the main problem seems not to be the distributed nature of agent-based systems but the agents´ autonomy, especially when agents have to act in a non-cooperative and non-deterministic environment because such situations require the ability to reason about the current situation context and draw own decisions in order to realize individual or common group goals. In our work we propose a model that is based on the Observe-Orient-Decide-Act Loop and the Belief-Desire-Intention Model and is completely realized with Reference Nets - a special kind of Object Petri Nets. It allows for the formal specification of Cognitive Decision Making processes together with inherent concurrencies as well as causal dependencies and facilitates automatic code generation. Furthermore, it enforces modeling with constrained resources in order to allow for practical model-checking.