A Solver for Modal Fixpoint Logics
A Solver for Modal Fixpoint Logics
复制标题
模态定点逻辑求解器
DOI：
10.1016/j.entcs.2010.04.008
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Martin Lange
中科院分区：
文献类型：
--
作者：
Oliver Friedmann;Martin Lange
我们提出了 MLSolver，一种用于解决模态不动点逻辑的可满足性和有效性问题的工具。底层技术基于通过无限（循环）画面的可满足性特征，其中分支具有反映无限中最小和最大固定点构造的再生的内线程结构。使用确定性奇偶自动机检查最小固定点展开的有根据性。这将可满足性和有效性问题简化为解决奇偶博弈问题。然后，MLSolver 使用奇偶游戏求解器来确定可满足性，并从奇偶游戏中的获胜策略中导出示例模型。当前支持的逻辑是模态和线性时间 μ 演算、CTL* 和 PDL（因此也支持 CTL 和 LTL）。 MLSolver 的设计允许以进一步模态定点逻辑的形式轻松扩展。
We present MLSolver, a tool for solving the satisfiability and validity problems for modal fixpoint logics. The underlying technique is based on characterisations of satisfiability through infinite (cyclic) tableaux in which branches have an inner thread structure mirroring the regeneration of least and greatest fixpoint constructs in the infinite. Well-foundedness for unfoldings of least fixpoints is checked using deterministic parity automata. This reduces the satisfiability and validity problems to the problem of solving a parity game. MLSolver then uses a parity game solver in order to decide satisfiability and derives example models from the winning strategies in the parity game. Currently supported logics are the modal and linear-time μ-calculi, CTL*, and PDL (and therefore also CTL and LTL). MLSolver is designed to allow easy extensions in the form of further modal fixpoint logics.
登录
查看更多内容
在没有确定性的情况下解决博弈
DOI：
--
发表时间：
2006
期刊：
Annual Conference for Computer Science Logic
影响因子：
--
作者：
T. Henzinger;Nir Piterman
通讯作者：
Nir Piterman
基于 Tableau 的即时 PDL 可满足性决策程序
DOI：
--
发表时间：
2007
期刊：
M4M
影响因子：
--
作者：
P. Abate;R. Goré;Florian Widmann
通讯作者：
Florian Widmann
捆绑 CTL 的 Tableau
影响因子：
0.7
作者：
Mark Reynolds
通讯作者：
Mark Reynolds
增强描述逻辑和命题动态逻辑之间的对应关系
DOI：
--
发表时间：
1994
期刊：
AAAI Conference on Artificial Intelligence
影响因子：
--
作者：
Giuseppe De Giacomo;M. Lenzerini
通讯作者：
M. Lenzerini