Model Checking of Constraint-Based Workflow Based on Linear Temporal Logic

机译：基于线性时间逻辑的约束工作流模型检查

获取原文

页面导航

摘要
著录项
相似文献
相关主题

摘要

The degree of flexibility of workflow management systems heavily influences the way business processes are executed. Constraint-based models are considered to be more flexible than traditional models because of their semantics: everything that does not violate constraints is allowed. More and more people use declarative languages to define workflow, such as linear temporal logic. But how to guarantee the correctness of the model based on the linear temporal logic is still a problem. This article proposes a way to verify the model based on Buchi automaton and gives the corresponding algorithms. Thus the verification of declarative workflow based on the linear temporal logic is solved.

机译：工作流管理系统的灵活性程度严重影响业务流程的执行方式。基于约束的模型被认为比传统模型更灵活，因为它们的语义：不允许违反约束的所有内容。越来越多的人使用陈述语言来定义工作流程，例如线性时间逻辑。但是如何保证基于线性时间逻辑的模型的正确性仍然是一个问题。本文提出了一种验证基于Buchi Automaton的模型的方法，并给出了相应的算法。因此，解决了基于线性时间逻辑的声明性工作流的验证。

著录项

来源
《International Conference on Management, Manufacturing and Materials Engineering》|2013年||共5页
会议地点
作者
Zhou Wenbo; Yao Shuzhen;
展开▼
作者单位

展开▼
会议组织
原文格式 PDF
正文语种
中图分类 TB3-53;
关键词
Constraint-based workflow; Linear temporal logic; Model checking; Buchi automata;

机译：基于约束的工作流程;线性时间逻辑;模型检查;Buchi自动机;

相似文献

外文文献
中文文献
专利

1. The detection of Udpstorm attacks based on model checking linear temporal logic [J] . Miaolei Deng, Kai Nie, Weijun Zhu, Automatic Control and Computer Sciences . 2017,第3期

机译：基于模型检查线性时间逻辑的UDPStorm攻击检测
2. BDD-versus SAT-based bounded model checking for the existential fragment of linear temporal logic with knowledge: algorithms and their performance [J] . Artur Meski, Wojciech Penczek, Maciej Szreter, Autonomous agents and multi-agent systems . 2014,第4期

机译：基于BDD相对于SAT的有界模型检验知识的线性时态逻辑存在性片段：算法及其性能
3. A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting [J] . Kyungmin Bae, José Meseguer Electronic Notes in Theoretical Computer Science . 2012,第12期

机译：基于重写的线性线性时序逻辑的基于模型的检查器
4. Model Checking of Constraint-Based Workflow Based on Linear Temporal Logic [C] . Zhou Wenbo, Yao Shuzhen International Conference on Management, Manufacturing and Materials Engineering . 2013

机译：基于线性时间逻辑的约束工作流模型检查
5. Model checking for a first-order temporal logic using multiway decision graphs. [D] . Xu, Ying. 1999

机译：使用多路决策图对一阶时间逻辑进行模型检查。
6. Model Checking Temporal Logic Formulas Using Sticker Automata [O] . Weijun Zhu, Changwei Feng, Huanmei Wu 2006

机译：使用贴纸自动机模型检查时间逻辑公式
7. BDD-versus SAT-based bounded model checking for the existential fragment of linear temporal logic with knowledge: algorithms and their performance [O] . Artur Mȩski, Wojciech Penczek, Maciej Szreter, 2013

机译：基于BDD相对于SAT的有界模型检验知识的线性时态逻辑存在性片段：算法及其性能
8. Model Checking Linear Temporal Logic Properties of Petri Nets with Fairness Constraints. [R] . Latvala, T. 2001

机译：具有公平约束的petri网线性时态逻辑性质模型检验。

Model Checking of Constraint-Based Workflow Based on Linear Temporal Logic

摘要

著录项

相似文献

相关主题

期刊订阅