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

timed soft concurrent constraint programs: An interleaved and a parallel approach

THEORY AND PRACTICE OF LOGIC programming 2015年第6期15卷 743-782页

作者： Bistarelli, Stefano Gabbrielli, Maurizio Meo, Maria Chiara Santini, Francesco Univ Perugia Dipartimento Matemat & Informat I-06123 Perugia Italy Univ Bologna Dipartimento Sci Informaz I-40126 Bologna Italy Univ G DAnnunzio Dipartimento Econ I-65127 Pescara Italy CWI NL-1098 XG Amsterdam Netherlands

We propose a timed and soft extension of concurrent constraint programming. The time extension is based on the hypothesis of bounded asynchrony: The computation takes a bounded period of time and is measured by a discrete global clock. Action prefixing is then considered as the syntactic marker that distinguishes a time instant from the next one. Supported by soft constraints instead of crisp ones, tell and ask agents are now equipped with a preference (or consistency) threshold, which is used to determine their success or suspension. In this paper, we provide a language to describe the agents' behavior, together with its operational and denotational semantics, for which we also prove the compositionality and correctness properties. After presenting a semantics using maximal parallelism of actions, we also describe a version for their interleaving on a single processor (with maximal parallelism for time elapsing). Coordinating agents that need to take decisions on both preference values and time events may benefit from this language.

关键词： Soft concurrent constraint programming timed concurrent constraint programming interleaving parallelism

来源：评论

学校读者我要写书评

暂无评论

Abstract interpretation of temporal concurrent constraint programs

引用

THEORY AND PRACTICE OF LOGIC programming 2015年第3期15卷 312-357页

作者： Falaschi, Moreno Olarte, Carlos Palamidessi, Catuscia Univ Siena Dipartimento Ingn Informaz & Sci Matemat I-53100 Siena Italy Pontificia Univ Javeriana Dept Elect & Ciencias Computac Cali Colombia Ecole Polytech INRIA Palaiseau France Ecole Polytech LIX Palaiseau France

timed concurrent constraint programming (tcc) is a declarative model for concurrency offering a logic for specifying reactive systems, i.e., systems that continuously interact with the environment. The universal tcc formalism (utcc) is an extension of tcc with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. In this paper we consider the denotational semantics for tcc, and extend it to a "collecting" semantics for utcc based on closure operators over sequences of constraints. Relying on this semantics, we formalize a general framework for data flow analyses of tcc and utcc programs by abstract interpretation techniques. The concrete and abstract semantics that we propose are compositional, thus allowing us to reduce the complexity of data flow analyses. We show that our method is sound and parametric with respect to the abstract domain. Thus, different analyses can be performed by instantiating the framework. We illustrate how it is possible to reuse abstract domains previously defined for logic programming to perform, for instance, a groundness analysis for tcc programs. We show the applicability of this analysis in the context of reactive systems. Furthermore, we also make use of the abstract semantics to exhibit a secrecy flaw in a security protocol. We also show how it is possible to make an analysis which may show that tcc programs are suspension-free. This can be useful for several purposes, such as for optimizing compilation or for debugging.

关键词： timed concurrent constraint programming process calculi abstract interpretation denotational semantics reactive systems

来源：评论

学校读者我要写书评

暂无评论

A Tool for Generating a Symbolic Representation of tccp Executions

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2009年 246卷 131-145页

作者： Lescaylle, Alexei Villanueva, Alicia Univ Politecn Valencia DSIC Camino Vera S-N E-46022 Valencia Spain

The timed concurrent constraint language (tccp) was defined by F. de Boer et al. as an extension of the concurrent constraint Paradigm (Saraswat, 1993) for specifying reactive and embedded systems. In this paper, we describe the StructGenerator system which, given the specification of a tccp program, constructs a symbolic representation (a tccp Structure) modeling the behavior of such tccp program. The resulting structure allows one to verify the program by using a model-checking algorithm. It is similar to a Kripke Structure but, due to the nature of the ccp model, it differs from the classical approach in some important points that will be described along the paper. The StructGenerator system, implemented in C++, takes as input a file containing the specification of a tccp program and generates the associated tccp Structure. Along the paper, we cover the design and implementation of StructGenerator. We also demonstrate its functionality carrying out the execution of two practical examples.

关键词： timed concurrent constraint programming symbolic representation tool demonstration

来源：评论

学校读者我要写书评

暂无评论

Modelling and implementing asynchronous timed multimedia frameworks using coordination principles

引用

FUTURE GENERATION COMPUTER SYSTEMS-THE INTERNATIONAL JOURNAL OF ESCIENCE 2005年第5期21卷 687-698页

作者： Papadopoulos, GA Univ Cyprus Dept Comp Sci CY-1678 Nicosia Cyprus

This paper combines work done in the areas of Artificial Intelligence, Multimedia Systems and Coordination programming to derive a framework for Distributed Multimedia Systems based on asynchronous timed computations expressed in a certain coordination formalism. More to the point, we propose the development of multimedia programming frameworks based on the declarative logic programming setting and in particular the framework of object-oriented timed concurrent constraint programming (OO-TCCP). The real-time extensions that have been proposed for the concurrent constraint programming framework are coupled with the object-oriented and inheritance mechanisms that have been developed for logic programs yielding an integrated declarative environment for multimedia objects modelling, composition and synchronisation. Furthermore, we show how the framework can be implemented in the general-purpose coordination language MANIFOLD without the need for using special architectures or real-time languages. (c) 2004 Elsevier B.V. All rights reserved.

关键词： multimedia programming timed concurrent constraint programming timed asynchronous languages coordination models distributed computing

来源：评论

学校读者我要写书评

暂无评论

Decidability of infinite-state timed CCP processes and first-order LTL

引用

THEORETICAL COMPUTER SCIENCE 2005年第3期330卷 577-607页

作者： Valencia, FD Ecole Polytech LIX CNRS F-91128 Palaiseau France

The ntcc process calculus is a timed concurrent constraint programming (ccp) model equipped with a first-order linear-temporal logic (LTL) for expressing process specifications. A typical behavioral observation in ccp is the strongest postcondition (sp,). The ntcc sp denotes the set of all infinite output sequences that a given process can exhibit. The verification problem is then whether the sequences in the sp of a given process satisfy a given ntcc LTL formula. This paper presents new positive decidability results for timed ccp as well as for LTL. In particular, we shall prove that the following problems are decidable: (1) the sp equivalence for the so-called locally-independent ntcc fragment;unlike other fragments for which similar results have been published. this fragment can specify infinite-state systems, (2) verification for locally-independent processes and negation-free first-orderformulae of the ntcc LTL, (3) implication for such formulae, (4) Satisfiability for a first-order fragment of Manna and Pnueli's LTL. The purpose of the last result is to illustrate the applicability of ccp to well-established formalisms for concurrency. (C) 2004 Elsevier B.V. All rights reserved.

关键词： process calculi timed concurrent constraint programming infinite-state systems temporal logic first-order LTL decidability

来源：评论

学校读者我要写书评

暂无评论

Automatic verification of timed concurrent constraint programs

引用

THEORY AND PRACTICE OF LOGIC programming 2006年第3期6卷 265-300页

作者： Falaschi, Moreno Villanueva, Alicia Univ Udine Dipartimento Matemat & Informat I-33100 Udine Italy Univ Politecn Valencia Dept Sistemas Informat & Computac E-46022 Valencia Spain

The language timed concurrent constraint (tccp) is the extension over time of the concurrent constraint programming (cc) paradigm that allows us to specify concurrent systems where timing is critical, for example reactive systems. Systems which may have an infinite number of states can be specified in tccp. Model checking is a technique which is able to verify finite-state systems with a huge number of states in an automatic way. In the last years several studies have investigated how to extend model checking techniques to systems with an infinite number of states. In this paper we propose an approach which exploits the computation model of tccp. constraint based computations allow us to define a methodology for applying a model checking algorithm to (a class of) infinite-state systems. We extend the classical algorithm of model checking for LTL to a specific logic defined for the verification of tccp and to the tccp Structure which we define in this work for modeling the program behavior. We define a restriction on the time in order to get a finite model and then we develop some illustrative examples. To the best of our knowledge this is the first approach that defines a model checking methodology for tccp.

关键词： automatic verification reactive systems timed concurrent constraint programming model checking

来源：评论

学校读者我要写书评

暂无评论

A Framework for Abstract Interpretation of timed concurrent constraint Programs

A Framework for Abstract Interpretation of Timed Concurrent ...

引用

11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative programming (PPDP 09)

作者： Falaschi, Moreno Olarte, Carlos Palamidessi, Catuscia Univ Siena Dipartimento Sci Matemat & Informat I-53100 Siena Italy

ISBN: (纸本)9781605585680

timed concurrent constraint programming (tcc) is a declarative model for concurrency offering a logic for specifying reactive systems, i.e. systems that continuously interact with the environment. The universal tcc formalism (utcc) is an extension of tcc with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. In this paper we consider the denotational semantics for tcc, and we extend it to a "collecting" semantics for utcc based on closure operators over sequences of constraints. Relying on this semantics, we formalize the first general frame-work for data flow analyses of tcc and utcc programs by abstract interpretation techniques. The concrete and abstract semantics we propose are compositional, thus allowing LIS to reduce the complexity of data flow analyses. We show that our method is sound and parametric w.r.t. the abstract domain. Thus, different analyses can be performed by instantiating the framework. We illustrate how it is possible to reuse abstract domains previously defined for logic programming, e.g., to perform a groundness analysis for tcc programs. We show the applicability of this analysis in the context of reactive systems. Furthermore, we make also use of the abstract semantics to exhibit a secrecy flaw in a security protocol. We have developed a prototypical implementation of our methodology and we have implemented the abstract domain for security to perform automatically the secrecy analysis.

关键词： timed concurrent constraint programming Process Calculi Abstract Interpretation Denotational Semantics Reactive Systems

来源：评论

学校读者我要写书评

暂无评论

Modelling and implementing asynchronous timed multimedia frameworks using coordination principles

Modelling and implementing asynchronous timed multimedia fra...

引用

7th International Conference on Parallel Computing Technologies (PaCT 2003)

作者： Papadopoulos, GA Univ Cyprus Dept Comp Sci CY-1678 Nicosia Cyprus

关键词： multimedia programming timed concurrent constraint programming timed asynchronous languages coordination models distributed computing

来源：评论

学校读者我要写书评

暂无评论

Decidability of infinite-state timed CCP processes and first-order LTL

Decidability of infinite-state timed CCP processes and first...

引用

10th International Workshop on Expressiveness in Concurrency (EXPRESS 2003)

作者： Valencia, FD Ecole Polytech LIX CNRS F-91128 Palaiseau France

关键词： process calculi timed concurrent constraint programming infinite-state systems temporal logic first-order LTL decidability

来源：评论

学校读者我要写书评

暂无评论

Modeling concurrent systems specified in a Temporal concurrent constraint language-I

引用

Electronic Notes in Theoretical Computer Science 2001年 48卷 197-210页

作者： Moreno Falaschi Alberto Policriti Alicia Villanueva Dipartimento di Matematica e Informatica Università di Udine Udine Italy

In this paper we present an approach to model concurrent systems specified in a temporal concurrent constraint language. Our goal is to construct a framework in which it is possible to apply the Model Checking technique to programs specified in such language. This work is the first step to the framework construction. We present a formalism to transform a specification into a tcc Structure. This structure is a graph representation of the program behavior. Our basic tool is the timed concurrent constraint programming (tcc) framework defined by Saraswat et al . to describe reactive systems. With this language we take advantage of both the natural properties of the declarative paradigm and of the fact that the notion of time is built into the semantics of the programming language. In fact, on this ground it becomes reasonable to introduce the idea of applying the technique of Model Checking to a finite time interval (introduced by the user). With this restriction we naturally force the space representing the behavior of the program to be finite and hence Model Checking algorithms to be applicable. The graph construction is a completely automatic process that takes as input the tcc specification.

关键词： timed concurrent constraint programming Reactive systems Model checking

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：