软件行为的模型推断是软件开发中一项重要的工作,已经提出许多模型推断算法在不同情况下帮助软件开发、测试和运维人员分析和调试软件系统。常用有限状态自动机表示软件行为模型,但是事件参数往往影响行为模型结构。因此,为了更准确地表达行为模型,现有方法常常将有限状态自动机推断算法扩展为扩展有限状态自动机。现有的扩展有限状态自动机推断算法难以满足不同使用场景的问题,将既有的有限状态自动机算法扩展为扩展有限状态自动机算法往往效率很低,需要专业人员进行大量返工设计开发。如何高效率将有限状态自动机算法进行扩展成为重要问题。同时,扩展有限状态自动机模型推断算法存在缺乏灵活性的问题,我们将针对控制流角度的灵活性问题进行分析解决。本文提出了一种叫做属性模型推断工具（Prop Mint）的声明式模型推断方法:（1）Prop Mint可以将有限状态自动机推断算法声明为扩展有限状态自动机推断算法。将Prop Mint应用于两种先进的有限状态自动机模型推断算法k Tails和Synoptic,使它们被声明为带有事件参数的扩展有限状态自动机推断算法。（2）将过程性扩展有限状态自动机模型推断算法解耦,使用户可以自由组合属性类型和属性实例,首次从控制流方面解决了扩展有限状态自动机推断算法的缺乏灵活性的问题。（3）通过声明式的方法优化了过程性模型推断的挖掘、合并等流程,在满足用户需求的前提下简化了推断过程,大幅提高了软件行为模型推断的效率,为动态分析软件行为提供了理论基础。通过实验我们验证Prop Mint的声明式方法在大多数情况下优于过程式实现。还发现在事件类型越少,事件日志越大的情况下,声明性Prop Mint算法的效率相比于过程性模型推断算法达到最佳。在实验中我们证明了Prop Mint声明的k Tails和Synoptic算法运行效率比过程性k Tails和Synoptic有大幅提升,同时分析了声明式模型推断算法高效的原因。