摘要:交替投影时序逻辑（alternating projection temporal logic，简称APTL）公式简单易懂，表达能力强；不仅可以描述经典时序逻辑LTL可以描述的性质，而且可以描述与区间相关的顺序和循环性质以及开放系统和多智能体系统中与博弈相关的性质.在验证系统是否满足所给的APTL公式所描述的性质之前需要检查公式的可满足性.根据检查APTL公式的可满足性的方法，开发实现了工具APTL2BCG.具体细节如下：首先，利用公式P的范式构造P的标记范式图（labeled normal form graph，简称LNFG）；然后，将LNFG转化为广义的基于并发博弈结构的交替Büchi自动机（generalized alternating Büchi automaton over concurrent game structure，简称GBCG）；最后，将GBCG转化为基于并发博弈结构的交替Büchi自动机（alternating Büchi automaton over concurrent game structure，简称BCG）并且化为最简形式并检查公式P的可满足性.
Abstract:Alternating projection temporal logic (APTL) has a concise syntax with strong expressive power. It is able to express not only properties specified in classical temporal logic LTL, but also interval related sequential and periodical properties, as well as game related properties of open systems and multi-agent systems. To verify whether a system satisfies an APTL formula, the satisfiability of the APTL formula should be checked. In this paper, based on the method for checking satisfiability of an arbitrary APTL formula provided, a supporting tool APTL2BCG has been developed. The details of implementation are given as follows. Firstly, LNFG of P is constructed according to the normal form of the formula P. Then, the LNFG is transformed to a generalized alternating Büchi automaton over concurrent game structure (GBCG). Finally, the alternating Büchi automaton is developed over concurrent game structure (BCG) from the obtained GBCG, and the BCG is simplified for checking the satisfiability of the formula P.
PDF全文下载地址:
http://jos.org.cn/jos/article/pdf/5459
删除或更新信息，请邮件至freekaoyan#163.com(#换成@)
APTL公式的可满足性检查工具
本站小编 Free考研考试/2022-01-02
相关话题/结构 逻辑 系统 智能 公式
领限时大额优惠券,享本站正版考研考试资料!
优惠券领取后72小时内有效，10万种最新考研考试考证类电子打印资料任你选。涵盖全国500余所院校考研专业课、200多种职业资格考试、1100多种经典教材，产品类型包含电子书、题库、全套资料以及视频，无论您是考研复习、考证刷题，还是考前冲刺等，不同类型的产品可满足您学习上的不同需求。 ...考试优惠券 本站小编 Free壹佰分学习网 2022-09-19一种嵌套中断系统的建模和分析方法
摘要:在嵌入式系统和各类操作系统中，中断机制是确保实时响应各类异步事件的重要方法.通常在处理一个中断事件的过程中，往往会有更紧迫的中断事件请求响应，因而发生中断嵌套.建模并验证嵌套中断系统是具有挑战性的工作.提出一种建模和验证嵌套中断系统的方法.首先，提出基于投影时序逻辑（projectiontem ...中科院软件研究所 本站小编 Free考研考试 2022-01-02机器人关节通信总线系统的建模与验证
摘要:高速串行现场总线（controllerareanetwork，简称CAN）被广泛部署到机器人通信系统中.而服务机器人任务具有并发性和高实时性的特点，因此，如何根据总线协议规范和应用需求精化设计模型，保证系统设计的正确性和实时性要求，避免设计阶段的漏洞十分必要.针对传统方法的局限性，提出使用形式 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02医学影像计算机辅助检测与诊断系统综述
摘要:计算机辅助检测/诊断（computer-aideddetection/diagnosis，简称CAD）能够提高诊断的准确性，减少假阳性的产生，为医生提供有效的诊断决策支持.旨在分析计算机辅助诊断工具的最新发展.以CAD研究较多的四大致命性癌症的发病医学部位为主线，按照不同的成像技术和病类，对目 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02基于同态加密系统的图像鲁棒可逆水印算法
摘要:同态加密技术可用于保护数据隐私并允许对密文数据进行算术操作，在云计算安全上有着很好的应用前景.针对云计算中的隐私保护和数据安全等问题，提出了一种基于同态加密系统的图像鲁棒可逆水印算法，主要思想为：（1）对原始图像进行分块和利用Paillier加密系统进行加密得到密文图像；（2）在加密域中，通过 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02基于创意序列学习的艺术风格学习与绘制系统
摘要:在众多传统艺术绘画形式中，笔触是被现代计算机绘画工具（GIMP、Photoshop和Painter）普遍采用的形式之一.创新性地提出了服务于非真实感渲染AI辅助艺术创作系统（A4）.系统能够实现自动生成特定艺术家风格的笔触效果.该系统在强化学习框架下，主要进行以下研究工作：（1）提出基于PGP ...中科院软件研究所 本站小编 Free考研考试 2022-01-02基于图结构的大数据分析与管理技术专刊前言
摘要:Abstract:PDF全文下载地址:http://jos.org.cn/jos/article/pdf/5458 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02分布式图处理系统技术综述
摘要:图作为一种基本的数据类型，是对现实世界中对象及其关联关系的一种抽象.现实中，许多科学问题都可以被模型化为图的问题，因此，对图数据进行分析非常重要.图数据分析在语义Web分析、社交网络、生物基因分析以及信息检索等领域有着广泛的应用.随着移动互联、物联网等信息技术的发展，图数据的规模处于持续增长的 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02基于MapReduce的图结构聚类算法
摘要:图结构聚类（SCAN）是一种著名的基于密度的图聚类算法，该算法不仅能够找到图中的聚类结构，而且还能发现图中的Hub节点和离群节点.然而，随着图数据规模越来越大，传统的SCAN算法的复杂度为O（m1.5）（m为图中边的条数），因此很难处理大规模的图数据.为了解决SCAN算法的可扩展性问题，提出一 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02多维图结构聚类的社交关系挖掘算法
摘要:社交关系的数据挖掘一直是大图数据研究领域中的热门问题.图聚类算法如SCAN（structuralclusteringalgorithmfornetwork）虽然可以迅速地从海量图数据中获得关系紧密的社区结构，但这类社区往往只表示了社交对象的聚集，无法反馈对象间的真实社交关系，如家庭成员、同事、 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02经验研究中情景感知需求获取与建模系统文献综述
摘要:情景感知（contextaware）的应用是当前的一个研究热点，但是，由于情景的复杂性和不确定性，如何获取这些应用的需求面临着巨大挑战，需求工程领域出现了大量的研究来解决这一挑战.使用系统文献综述（systematicliteraturereview）的方法首先分析了不同情景维度对需求获取与建 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02
