主体计划的Petri网方法及正确性验证

摘要

主体计划的生成问题是多主体系统实现的一个关键问题。为了实现多主体系统中的计划自动生成以及对生成的计划进行验证,以任务有效分解的Petri网模型为基础,提出了计划提取的方法并对相关的正确性运用同步器进行验证.首先,通过对网系统的可达性分析得到所有计划的集合,组成多主体系统的计划库.其次,根据同步网的相关思想,对计划库中的每一个计划的正确性进行了形式化的验证,从而为多主体系统的实现提供了保证.