检索结果-内蒙古大学图书馆

ARTIFICIAL INTELLIGENCE 2025年 338卷

作者： Aguilera, Juan Pablo Dieguez, Martin Fernandez-Duque, David McLean, Brett Univ Ghent Dept Math WE16 Ghent Belgium Vienna Univ Technol Inst Discrete Math & Geometry Vienna Austria Univ Angers LERIA Angers France Univ Barcelona Dept Philosophy Barcelona Spain

We investigate a version of linear temporal logic whose propositional fragment is G & ouml;del-Dummett logic (which is well known both as a superintuitionistic logic and a t-norm fuzzy logic). We define the logic using two natural semantics: first a real-valued semantics, where statements have a degree of truth in the real unit interval, and second a 'bi-relational' semantics. We then show that these two semantics indeed define one and the same logic: the statements that are valid for the real-valued semantics are the same as those that are valid for the bi-relational semantics. This G & ouml;del temporal logic does not have any form of the finite model property for these two semantics: there are non-valid statements that can only be falsified on an infinite model. However, by using the technical notion of a quasimodel, we show that every falsifiable statement is falsifiable on a finite quasimodel, yielding an algorithm for deciding if a statement is valid or not. Later, we strengthen this decidability result by giving an algorithm that uses only a polynomial amount of memory, proving that G & ouml;del temporal logic is PSPACE-complete. We also provide a deductive calculus for G & ouml;del temporal logic, and show this calculus to be sound and complete for the above-mentioned semantics, so that all (and only) the valid statements can be proved with this calculus.

关键词： G & ouml del-Dummett logic linear temporal logic Automated temporal reasoning PSPACE-complete Hilbert-style deductive calculus

来源：评论

学校读者我要写书评

暂无评论

linear temporal logic LTL_K extended by Multi-Agent logic K_n with Interacting Agents

引用

JOURNAL OF logic AND COMPUTATION 2009年第6期19卷 989-1017页

作者： Rybakov, Vladimir Manchester Metropolitan Univ Dept Comp & Math Manchester M1 5GD Lancs England Siberian Fed Univ Krasnoyarsk Russia

We study an extension LTLK of the linear temporal logic LTL by implementing multi-agent knowledge logic KD45(m) (which is often referred as multi-modal logic S5(m)). The temporal language of our logic adapts the operations U (until) and N (next) and uses new temporal operations: U-w-weak until, and U-s-strong until. We also employ the standard agents' knowledge operations K-i from the multi-agent logic KD45(m) and extend them with an operation IntK responsible for knowledge obtained via interaction of agents. The semantic models for LTLK are Kripke/Hintikka-like structures N-C based on the linear time. Structures N-C use i is an element of N as indexes for time, and the base set of any N-C consists of clusters C(i) (for all i is an element of N) containing all possible states at the time i. Agents' knowledge is modelled in time clusters C(i) via agents' knowledge accessibility relations R-j. The logic LTLK is the set of all formulas which are valid (true) in all such models N-C w.r.t. all possible valuations. We prove that LTLK is decidable: we reduce the decidability problem to verification of validity for special normal reduced forms of rules in specific models (not LTLK models) of size single-exponential in size of the rules. Furthermore. we extend these results to a linear temporal logic LTLK(Z) based on the time flow indexed by all integer numbers (with additional operations Since and Previous). Also we show that LTLK has the finite model property (fmp) while LTLK(Z) has no standard fmp.

关键词： linear temporal logic modal logics multi-agent logic interacting agents decidability algorithms inference rules

来源：评论

学校读者我要写书评

暂无评论

linear temporal logic with until and next, logical consecutions

引用

ANNALS OF PURE AND APPLIED logic 2008年第1期155卷 32-45页

作者： Rybakov, V. Manchester Metropolitan Univ Dept Comp & Math Manchester M1 5GD Lancs England Siberian Fed Univ Krasnoyarsk Russia

While specifications and verifications of concurrent systems employ linear temporal logic (LTL), it is increasingly likely that logical consequence in LTL will be used in the description of computations and parallel reasoning. Our paper considers logical consequence in the standard LTL with temporal operations U (until) and N (next). The prime result is an algorithm recognizing consecutions admissible in LTL, so we prove that LTL is decidable w.r.t. admissible inference rules. As a consequence we obtain algorithms verifying the validity of consecutions in LTL and solving the satisfiability problem. We start by a simple reduction of logical consecutions (inference rules) of LTL to equivalent ones in the reduced normal form (which have uniform structure and consist of formulas of temporal degree 1). Then we apply a semantic technique based on LTL-Kripke structures with formula definable subsets. This yields necessary and sufficient conditions for a consecution to be not admissible in LTL. These conditions lead to an algorithm which recognizes consecutions (rules) admissible in LTL by verifying the validity of consecutions in special finite Kripke structures of size square polynomial in reduced normal forms of the consecutions. As a consequence, this also solves the satisfiability problem for LTL. (C) 2008 Elsevier B.V. All rights reserved.

关键词： Algorithms linear temporal logic Admissible consecutions logical consequence Admissible inference rules

来源：评论

学校读者我要写书评

暂无评论

linear temporal logic Specification of Bounded Counter Machines

引用

AUTOMATIC CONTROL AND COMPUTER SCIENCES 2023年第7期57卷 683-695页

作者： Kuzmin, E. V. Yaroslavl State Univ Yaroslavl 150003 Russia

This article revises the results of work devoted to representing the behavior of a program system as a set of formulae of linear temporal logic (LTL), followed by the use of this representation to verify the satisfiability of the program properties of the system by proving the validity of logical inferences expressed in terms of the LTL. This logic is applied to bounded Minsky counter machines considered as program systems whose behavior must be specified. Earlier on, a special pseudooperator was introduced for referring to previous values of variables used in elementary propositions when working with the LTL temporal logic as a program logic. Even though this pseudooperator is easy to implement in the Cadence SMV verifier when proving the validity of logical LTL inferences, the classical definition of the LTL does not imply its presence. This article will use only binary variables to build the LTL specification for the behavior of a bounded counter machine. Previous values of these variables will be tracked through the appropriate formulas exclusively within the LTL itself.

关键词： nonclassical logic linear temporal logic counter machines LTL specification

来源：评论

学校读者我要写书评

暂无评论

linear temporal logic with until and before on integer numbers, deciding algorithms

Linear temporal logic with until and before on integer numbe...

引用

International Computer Science Symposium in Russia (CSR 2006)

作者： Rybakov, V. Manchester Metropolitan Univ Dept Comp & Math Manchester M1 5GD Lancs England

ISBN: (纸本)3540341668

As specifications and verifications of concurrent systems employ linear temporal logic (LTL), it is increasingly likely that logical consequence in LTL will be used in description of computations and parallel reasoning. We consider the linear temporal logic LTLN, N-1U, B (Z) extending the standard LTL by operations B (before) and N-1 (previous). Two sorts of problems are studied: (i) satisfiability and (ii) description of logical consequence in LTLN, N-1U, B (Z) via admissible logical consecutions (inference rules). The model checking for LTL is a traditional way of studying such logics. Most popular technique based on automata was developed by *** (cf. [39,61). Our paper uses a reduction of logical consecutions and formulas of LTL to consecutions of a uniform form consisting of formulas of temporal degree 1. Based on technique of Kripke structures, we find necessary and sufficient conditions for a consecution to be not admissible in LTLN, N-1U, B (Z). This provides an algorithm recognizing consecutions (rules) admissible in LTLN, N-1U, B (Z) by Kripke structures of size linear in the reduced normal forms of the initial consecutions. As an application, this algorithm solves also the satisfiability problem for LTLN, N-1U, B (Z).

关键词： logic in computer science algorithms linear temporal logic logical consequence inference rules consecutions admissible rules

来源：评论

学校读者我要写书评

暂无评论

linear temporal logic Applied to Component-Based Software Architectural Models Specified Through ρ_arq Calculus 5th

Linear Temporal Logic Applied to Component-Based Software Ar...

引用

5th Workshop on Engineering Applications (WEA)

作者： Javier Puentes, Oscar Alberto Diosa, Henry Univ Dist Francisco Jose de Caldas Res Grp ARQUISOFT Fac Engn Bogota Colombia

ISBN: (纸本)9783030003500;9783030003494

This paper reports a mechanism to incorporate linear temporal logic (LTL) for a component-based software architectural configuration specified by the rho(arq)-calculus. This process was made through the translation of the system definition, structure and behavior, to Atomic Propositions Transition System (APTS), upon which, the verification of one property was performed using LTL. The PintArq software application was extended to support this mechanism. One example ilustrates the verification of responsiveness, a subtype of liveness property.

关键词： rho(arq) calculus Component-based software Architectural execution flow linear temporal logic Model checking

来源：评论

学校读者我要写书评

暂无评论

linear temporal logic Satisfaction in Adversarial Environments Using Secure Control Barrier Certificates 10th

Linear Temporal Logic Satisfaction in Adversarial Environmen...

引用

10th International Conference on Decision and Game Theory for Security (GameSec)

作者： Ramasubramanian, Bhaskar Niu, Luyao Clarke, Andrew Bushnell, Linda Poovendran, Radha Univ Washington Dept Elect & Comp Engn Seattle WA 98195 USA Worcester Polytech Inst Dept Elect & Comp Engn Worcester MA 01609 USA

ISBN: (纸本)9783030324308;9783030324292

This paper studies the satisfaction of a class of temporal properties for cyber-physical systems (CPSs) over a finite-time horizon in the presence of an adversary, in an environment described by discrete-time dynamics. The temporal logic specification is given in safe-LTLF, a fragment of linear temporal logic over traces of finite length. The interaction of the CPS with the adversary is modeled as a two-player zero-sum discrete-time dynamic stochastic game with the CPS as defender. We formulate a dynamic programming based approach to determine a stationary defender policy that maximizes the probability of satisfaction of a safe - LTLF formula over a finite time-horizon under any stationary adversary policy. We introduce secure control barrier certificates (S-CBCs), a generalization of barrier certificates and control barrier certificates that accounts for the presence of an adversary, and use S-CBCs to provide a lower bound on the above satisfaction probability. When the dynamics of the evolution of the system state has a specific underlying structure, we present a way to determine an S-CBC as a polynomial in the state variables using sum-of-squares optimization. An illustrative example demonstrates our approach.

关键词： linear temporal logic safe - LTLF Dynamic programming Secure control barrier certificate Sum-of-squares optimization

来源：评论

学校读者我要写书评

暂无评论

Modeling compliance specifications in linear temporal logic, event processing language and property specification patterns: a controlled experiment on understandability

引用

SOFTWARE AND SYSTEMS MODELING 2019年第6期18卷 3331-3371页

作者： Czepa, Christoph Amiri, Amirali Ntentos, Evangelos Zdun, Uwe Univ Vienna Fac Comp Sci Res Grp Software Architecture Wahringerstr 29 A-1090 Vienna Austria

Mature verification and monitoring approaches, such as complex event processing and model checking, can be applied for checking compliance specifications at design time and runtime. Little is known about the understandability of the different formal and technical languages associated with these approaches. This uncertainty regarding understandability might be a major obstacle for the broad practical adoption of those techniques. This article reports a controlled experiment with 215 participants on the understandability of modeling compliance specifications in representative modeling languages, namely linear temporal logic (LTL), the complex event processing-based event processing language (EPL) and property specification patterns (PSP). The formalizations in PSP were overall more correct. That is, the pattern-based approach provides a higher level of understandability than EPL and LTL. More advanced users, however, seemingly are able to cope equally well with PSP and EPL in modeling compliance specifications.

关键词： Controlled experiment Understandability linear temporal logic Property specification patterns Complex event processing Event processing language

来源：评论

学校读者我要写书评

暂无评论

Non-transitive linear temporal logic and logical knowledge operations

引用

JOURNAL OF logic AND COMPUTATION 2016年第3期26卷 945-958页

作者： Rybakov, Vladimir V. Manchester Metropolitan Univ Sch Comp Math & DT John Dalton BldgChester St Manchester M1 5GD Lancs England

We study a linear temporal logic LTLNT with non-transitive time (with NEXT and UNTIL) and possible interpretations for logical knowledge operations in this approach. We assume time to be non-transitive, linear and discrete, it is a major innovative part of our article. Motivation for our approach that time might be non-transitive and comments on possible interpretations of logical knowledge operations are given. The main result of Section 5 is a solution of the decidability problem for LTLNT, we find and describe in details the decision algorithm. In Section 6 we introduce non-transitive linear temporal logic LTLNT(m) with uniform bound (m) for non-transitivity. We compare it with standard linear temporal logic LTL and the logic LTLNT-where non-transitivity has no upper bound-and show that LTLNT may be approximated by logics LTLNT(m). Concluding part of the article contains a list of open interesting problems.

关键词： linear temporal logic non-transitive time knowledge logical knowledge operations deciding algorithms

来源：评论

学校读者我要写书评

暂无评论

On the complexity of linear temporal logic with team semantics

引用

THEORETICAL COMPUTER SCIENCE 2020年 837卷 1-25页

作者： Lack, Martin Leibniz Univ Hannover Inst Theoret Informat Appelstr 4 D-30167 Hannover Germany

A specification given as a formula in linear temporal logic (LTL) defines a system by its set of traces. However, certain features such as information flow security constraints are rather modeled as so-called hyperproperties, which are sets of sets of traces. One logical approach to this is team logic, which is a logical framework for the specification of dependence and independence of information. LTL with team semantics has recently been discovered as a logic for hyperproperties. We study the complexity theoretic aspects of LTL with so-called synchronous team semantics and Boolean negation, and prove that both its model checking and satisfiability problems are highly undecidable, and equivalent to the decision problem of third-order arithmetic. Furthermore, we prove that this complexity already appears at small temporal depth and with only the "future" modality F. Finally, we also introduce a team-semantical generalization of stutter-invariance. (c) 2020 Elsevier B.V. All rights reserved.

关键词： linear temporal logic Team semantics Complexity

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：