由于多主体系统(MAS)能体现人类的社会智能、具有很大的灵活性和适应性，可以广泛地运用于构建开放、动态的软件系统，所以成为人工智能研究的核心领域之一。而使用形式化工具对多主体系统中相关问题的形成、描述和分解以及结果的合成等问题的分析是多主体系统亟待解决的关键问题之一。本文以多个主体协作完成一个大目标为研究对象，建立了任务有效分解的Petri网模型，验证了模型具有的性质，并在此基础上提出了基于合同网协议思想的任务动态分配的Petri网模型和计划实施的Petri网模型，并进行了相关性质的分析与验证。 本文的研究成果主要包括以下几个方面： 1) 详细描述了保证无歧义情况下的逻辑与／或树的语义，并给出了逻辑与／或树的生成算法，提出了将任务分解的逻辑与／或树转换为Petri网模型的转换规则。 2) 通过剔除不合理的任务分解结构得到任务有效分解的Petri网模型，详细分析了任务有效分解的Petri网系统的活性，并指出了活性与有效的任务分解之间的联系；通过任务有效分解的Petri网系统的可达性分析，得到所有可行的解决问题的实施计划，同时运用网逻辑对计划的正确性进行验证，并对任务间的并发关系给出判定定理，最后给出一个诠释性的例子。 3) 采用逐级细化的建模思想建立任务动态分配的Petri网模型。任务动态分配的Petri网模型主要从两个层面进行考虑：从社会层面出发的宏观模型和从主体层面出发的微观模型。宏观模型中包括了具有固定数目的工作者主体和具有不定数目的工作者主体的两种多主体竞标模型，通过Petri网刻画了多主体之间的协作；微观模型中主要介绍了基于BDI结构的主体Petri网模型，研究了各主体内部心智状态的变化。同时详细刻画了两个层次模型的动态语义，并根据保性的Petri网细化运算分析了任务动态分配的Petri网模型的相关性质。 4) 给出了计划实施的扩展的同步网系统定义，使主体计划的实施得到正确的监控。在此基础上描述了网系统的动态语义，并给出了主体间并发的判定定理。 综上所述，本文对任务的分解以及任务在多主体间的动态分配作出了一定的研究。这些研究还有许多问题值得探讨，还有待进一步的研究。