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

A Framed temporal logic programming Language

Journal of Computer Science & Technology 2004年第3期19卷 341-351页

作者： Zhen-HuaDuan MaciejKoutny UniversityofNewcastleuponTyne NewcastleuponTyneNE17RUU.K. XidianUniversity Xi＇an710071P.R.China／／LaboratoryofComputerScienceISCASBeijing100080P.R.China

We discuss the projection temporal logic (PTL), based on a primitiveprojection operator, prj. A framing technique is also presented, using which a synchronizationoperator, await, is defined within the underlying logic. A framed temporal logic programminglanguage (FTLL) is presented. To illustrate how to use both the language and framing technique, someexamples are given.

关键词： temporal logic temporal logic programming frame projection concurrency

来源：评论

学校读者我要写书评

暂无评论

MSVL： a typed language for temporal logic programming

引用

Frontiers of Computer Science 2017年第5期11卷 762-785页

作者： Xiaobing WANG Cong TIAN Zhenhua DUAN Liang ZHAO ICTT and ISN Lab Xidian University Xi'an 710071 China

The development of types is an important but challenging issue in temporal logic programming. In this paper, we investigate how to formalize and implement types in the temporal logic programming language MSVL, which is an executable subset of projection temporal logic （PTL）. Specifically, we extend MSVL with a few groups of types including basic data types, pointer types and struct types. On each type, we specify the domain of values and define some standard operations in terms of logic functions and predicates. Then, it is feasible to formalize statements of type declaration of program variables and statements of struct definitions as logic formulas. As the implementation of the theory, we extend the MSV toolkit with the support of modeling, simulation and verification of typed MSVL programs. Applications to the construction of AVL tree and ordered list show the practicality of the language.

关键词： type temporal logic programming MSVL type declaration struct definition

来源：评论

学校读者我要写书评

暂无评论

Framed temporal logic programming

引用

SCIENCE OF COMPUTER programming 2008年第1期70卷 31-61页

作者： Duan, Zhenhua Yang, Xiaoxiao Koutny, Maciej Xidian Univ Inst Comp Theory & Technol Xian 710071 Peoples R China Newcastle Univ Sch Comp Sci Newcastle Upon Tyne NE1 7RU Tyne & Wear England

A Projection temporal logic is discussed and some of its laws are given. After that, an executable temporal logic programming language, called Framed Tempura, is formalized. A minimal model-based approach for framing in temporal logic programming is presented. Since framing destroys monotonicity, canonical models - used to define the semantics of non-framed programs - are no longer appropriate. To deal with this, a minimal model theory is developed, using which the temporal semantics of framed programs is captured. The existence of a minimal model for a given framed program is demonstrated. A synchronous communication mechanism for concurrent programs is provided by means of the framing technique and minimal model semantics. (C) 2007 Elsevier B.V. All rights reserved.

关键词： temporal logic programming framing minimal model monotonicity synchronization communication semantics

来源：评论

学校读者我要写书评

暂无评论

Stratified negation in temporal logic programming and the cycle-sum test

引用

THEORETICAL COMPUTER SCIENCE 2001年第1-2期254卷 663-676页

作者： Rondogiannis, P Univ Athens Dept Informat Athens 15784 Greece

We consider stratified negation in temporal logic programming. We demonstrate that the cycle-sum test (which was initially proposed for detecting deadlocks in the context of temporal functional programming) can also be used as a syntactic stratification test for temporal logic programming. Therefore, on the one hand we exhibit a class of temporal logic programs with negation which have a well-defined semantics, and on the other hand we provide further evidence that the cycle-sum test is a fundamental one in the area of temporal programming. (C) 2001 Elsevier Science B.V. All rights reserved.

关键词： temporal logic programming negation stratification cycle-sum test

来源：评论

学校读者我要写书评

暂无评论

A proof procedure for temporal logic programming

引用

INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE 2004年第2期15卷 417-443页

作者： Gergatsoulis, M Nomikos, C Ionian Univ Dept Arch & Lib Sci Corfu 49100 Greece Univ Ioannina Dept Comp Sci GR-45110 Ioannina Greece

In this paper, we propose a new resolution proof procedure for the branching-time logic programming language Cactus. The particular strength of the new proof procedure, called CSLD-resolution, is that it can handle, in a more general way, open-ended queries, i.e. goal clauses that include atoms which do not refer to specific moments in time, without the need of enumerating all their canonical instances. We also prove soundness, completeness and independence of the computation rule for CSLD-resolution. The new proof procedure overcomes the limitations of a family of proof procedures for temporal logic programming languages, which were based on the notions of canonical program and goal clauses. Moreover, it applies directly to Chronolog programs and it can be easily extended to apply to multi-dimensional logic programs as well as to Chronolog(MC) programs.

关键词： temporal logic programming proof procedures branching-time theorem proving

来源：评论

学校读者我要写书评

暂无评论

logical Foundations for More Expressive Declarative temporal logic programming Languages

引用

ACM TRANSACTIONS ON COMPUTATIONAL logic 2013年第4期14卷 28-28页

作者： Gaintzarain, Jose Lucio, Paqui Univ Basque Country EUITI Bilbao Dept Comp Languages & Syst Bilbao 48013 Spain Univ Basque Country Fac Informat Dept Comp Languages & Syst San Sebastian 20018 Spain

In this article, we present a declarative propositional temporal logic programming language called TeDiLog that is a combination of the temporal and disjunctive paradigms in logic programming. TeDiLog is, syntactically, a sublanguage of the well-known Propositional Linear-time temporal logic (PLTL). TeDiLog allows both eventualities and always-formulas to occur in clause heads and also in clause bodies. To the best of our knowledge, TeDiLog is the first declarative temporal logic programming language that achieves this high degree of expressiveness. We establish the logical foundations of our proposal by formally defining operational and logical semantics for TeDiLog and by proving their equivalence. The operational semantics of TeDiLog relies on a restriction of the invariant-free temporal resolution procedure for PLTL that was introduced by Gaintzarain et al. in [2013]. We define a fixpoint semantics that captures the reverse (bottom-up) operational mechanism and prove its equivalence with the logical semantics. We also provide illustrative examples and comparison with other proposals.

关键词： Algorithms Languages Theory Disjunctive logic programming invariant-free clausal temporal resolution linear-time temporal logic operational and logical semantics refutation procedure temporal logic programming

来源：评论

学校读者我要写书评

暂无评论

temporal disjunctive logic programming

引用

NEW GENERATION COMPUTING 2001年第1期19卷 87-100页

作者： Gergatsoulis, M Rondogiannis, P Panayiotopoulos, T NCSR Demokritos Inst Informat & Telecommun GR-15310 Athens Greece Univ Ioannina Dept Comp Sci GR-45110 Ioannina Greece Univ Piraeus Dept Informat Piraeus 18534 Greece

In this paper we introduce the logic programming language Disjunctive Chronology which combines the programming paradigms of temporal and disjunctive logic programming. Disjunctive Chronolog is capable of ex pressing dynamic behaviour as well as uncertainty, two notions that are very common in a variety of real systems. We present the minimal temporal model semantics and the fixpoint semantics for the new programming language and demonstrate their equivalence. We also show how proof procedures developed for disjunctive logic programs can be easily extended to apply to Disjunctive Chronolog programs.

关键词： temporal logic programming disjunctive logic programming semantics proof procedures

来源：评论

学校读者我要写书评

暂无评论

A temporal programming model with atomic blocks based on projection temporal logic

引用

Frontiers of Computer Science 2014年第6期8卷 958-976页

作者： Xiaoxiao YANG Yu ZHANG Ming FU Xinyu FENG State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Beijing 100190 China Suzhou Institute for Advanced Study University of Science & Technology of China SuZhou 215123 China

Atomic blocks, a high-level language construct that allows programmers to explicitly specify the atomicity of operations without worrying about the implementations, are a promising approach that simplifies concurrent programming. On the other hand, temporal logic is a successful model in logic programming and concurrency verification, but none of existing temporal programming models supports concurrent programming with atomic blocks yet. In this paper, we propose a temporal programming model （αPTL） which extends the projection temporal logic （PTL） to support concurrent programming with atomic blocks. The novel construct that formulates atomic execution of code blocks, which we call atomic interval formulas, is always interpreted over two consecutive states, with the internal states of the block being abstracted away. We show that the framing mechanism in projection temporal logic also works in the new model, which consequently supports our development of an executive language. The language supports concurrency by introducing a loose interleaving semantics which tracks only the mutual exclusion between atomic blocks. We demonstrate the usage of αPTL by modeling and verifying both the fine-grained and coarse-grained concurrency.

关键词： atomic blocks semantics temporal logic programming verification framing

来源：评论

学校读者我要写书评

暂无评论

THE COMPUTATIONAL-COMPLEXITY OF SATISFIABILITY OF temporal HORN FORMULAS IN PROPOSITIONAL LINEAR-TIME temporal logic

引用

INFORMATION PROCESSING LETTERS 1993年第3期45卷 131-136页

作者： CHEN, CC LIN, IP Department of Computer Science and Information Engineering National Taiwan University Taipei Taiwan

The complexity of the satisfiability problem for 2 Horn fragments in propositional linear-time temporal logic is investigated. The first one contains 2 temporal connectives - eventuality and always only - and the 2nd one contains an additional next-time connective. It has been shown that the satisfiability problem for linear-time temporal logic whose temporal connectives include eventuality and always only is NP-complete and is PSPACE-complete if additional next-time connective is permitted, according to Sistla and Clarke (1985). It is shown that the complexity of the satisfiability problem remains unchanged even if the input is restricted to temporal Horn formulas. In other words, if the next-time connective is not allowed to occur in temporal Horn formulas, the problem is NP-complete; otherwise, it is PSPACE-complete.

关键词： COMPUTATIONAL COMPLEXITY temporal logic temporal HORN FORMULA temporal logic programming SATISFIABILITY

来源：评论

学校读者我要写书评

暂无评论

A mechanism of function calls in MSVL

引用

THEORETICAL COMPUTER SCIENCE 2016年 654卷 11-25页

作者： Zhang, Nan Duan, Zhenhua Tian, Cong Xidian Univ Inst Comp Theory & Technol Xian 710071 Peoples R China Xidian Univ ISN Lab Xian 710071 Peoples R China

Modeling, Simulation and Verification Language (MSVL) is a useful formalism for specification and verification of concurrent systems. To make it more practical and easier to use, we extend MSVL with external and internal function calls. To do so, the syntax of function definitions and function calls is formalized. Then, the syntax of expressions in MSVL is extended by including function calls. Further, the evaluation rules are redefined. Moreover, the set of statements in MSVL is also extended and the semantics of function call statements is formalized. In addition, the existence of minimal models of MSVL programs involving new added statements is proved. Finally, an example is given to illustrate how to interpret function calls in practice with MSVL. (C) 2016 Elsevier B.V. All rights reserved.

关键词： temporal logic programming Projection Function call Modeling Simulation Verification

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：