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

A concurrent constraint programming interpretation of access permissions

THEORY AND PRACTICE OF LOGIC programming 2018年第2期18卷 252-295页

作者： Olarte, Carlos Pimentel, Elaine Rueda, Camilo Univ Fed Rio Grande do Norte ECT Natal RN Brazil Univ Fed Rio Grande do Norte DMAT Natal RN Brazil Pontificia Univ Javeriana Cali DECC Valle Del Cauca Colombia

A recent trend in object-oriented programming languages is the use of access permissions (APs) as an abstraction for controlling concurrent executions of programs. The use of AP source code annotations defines a protocol specifying how object references can access the mutable state of objects. Although the use of APs simplifies the task of writing concurrent code, an unsystematic use of them can lead to subtle problems. This paper presents a declarative interpretation of APs as linear concurrent constraint programs (1cc). We represent APs as constraints (i.e., formulas in logic) in an underlying constraint system whose entailment relation models the transformation rules of APs. Moreover, we use processes in 1cc to model the dependencies imposed by APs, thus allowing the faithful representation of their flow in the program. We verify relevant properties about AP programs by taking advantage of the interpretation of 1cc processes as formulas in Girard's intuitionistic linear logic (ILL). Properties include deadlock detection, program correctness (whether programs adhere to their AP specifications or not), and the ability of methods to run concurrently. By relying on a focusing discipline for ILL, we provide a complexity measure for proofs of the above-mentioned properties. The effectiveness of our verification techniques is demonstrated by implementing the Alcove tool that includes an animator and a verifier. The former executes the 1cc model, observing the flow of APs, and quickly finding inconsistencies of the APs vis-a-vis the implementation. The latter is an automatic theorem prover based on ILL.

关键词： access permissions concurrent constraint programming linear logic focusing

来源：评论

学校读者我要写书评

暂无评论

Subexponential concurrent constraint programming

引用

THEORETICAL COMPUTER SCIENCE 2015年 606卷 98-120页

作者： Olarte, Carlos Pimentel, Elaine Nigam, Vivek Univ Fed Rio Grande do Norte BR-59072970 Natal RN Brazil Univ Fed Paraiba BR-58059900 Joao Pessoa Paraiba Brazil

In previous works we have shown that linear logic with subexponentials (SELL), a refinement of linear logic, can be Used to specify emergent features of concurrent constraint programming (CCP) languages, such as preferences and spatial, epistemic and temporal modalities. In order to do so, we introduced a number of extensions to SELL, such as subexponential quantifiers for the specification of modalities, and more elaborated subexponential structures for the specification of preferences. These results provided clear proof theoretic foundations to existing systems. This paper goes in the opposite direction, answering positively the question: can the proof theory of linear logic with subexponentials contribute to the development of new CCP languages? We propose a CCP language with the following powerful features: 1) computational spaces where agents can tell and ask preferences (soft-constraints);2) systems where spatial and temporal modalities can be combined;3) shared spaces for communication that can be dynamically established;and 4) systems that can dynamically create nested spaces. In order to provide the proof theoretic foundations for such a language, we propose a unified logical framework (SELLS(sic)) combining the extensions of linear logic with subexponentials mentioned above, and showing that this new framework has interesting proof theoretical properties such as cut-elimination and a sound and complete focused proof system. (C) 2015 Elsevier B.V. All rights reserved.

关键词： Linear logic concurrent constraint programming Proof systems

来源：评论

学校读者我要写书评

暂无评论

Efficient algorithms for program equivalence for confluent concurrent constraint programming

引用

SCIENCE OF COMPUTER programming 2015年第Part1期111卷 135-155页

作者： Pino, Luis F. Bonchi, Filippo Valencia, Frank INRIA DGA F-91128 Palaiseau France Ecole Polytech CNRS LIX UMR X 7161 F-91128 Palaiseau France Univ Lyon ENS Lyon LIP UMR 5668CNRSENS LyonUCBLINRIA F-69364 Lyon France Ecole Polytech CNRS F-91128 Palaiseau France

concurrent constraint programming (CCP) is a well-established declarative framework from concurrency theory. Its foundations and principles e.g., semantics, proof systems, axiomatizations, have been thoroughly studied for over the last two decades. In contrast, the development of algorithms and automatic verification procedures for CCP have hitherto been far too little considered. To the best of our knowledge there is only one existing verification algorithm for the standard notion of CCP program (observational) equivalence. In this paper we first show that this verification algorithm has an exponential-time complexity even for programs from a representative sub-language of CCP;the summation-free fragment (CCP\+). We then significantly improve on the complexity of this algorithm by providing two alternative polynomial-time decision procedures for CCP\+ program equivalence. Each of these two procedures has an advantage over the other. One has a better time complexity. The other can be easily adapted for the full language of CCP to produce significant state space reductions. The relevance of both procedures derives from the importance of CCP\+. This fragment, which has been the subject of many theoretical studies, has strong ties to first-order logic and an elegant denotational semantics, and it can be used to model real-world situations. Its most distinctive feature is that of confluence, a property we exploit to obtain our polynomial procedures. Finally, we also study the congruence issues regarding CCP's program equivalence. (C) 2015 Elsevier B.V. All rights reserved.

关键词： concurrent constraint programming Bisimulation Partition refinement Observational equivalence

来源：评论

学校读者我要写书评

暂无评论

A Symbolic Model for Timed concurrent constraint programming

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2015年 312卷 161-177页

作者： Arias, Jaime Guzman, Michell Olarte, Carlos Univ Bordeaux LaBRI UMR 5800 F-33400 Talence France CNRS LaBRI UMR 5800 F-33400 Talence France Univ Valle DECC Cali Colombia Univ Fed Rio Grande do Norte ECT BR-59072970 Natal RN Brazil Pontificia Univ Javeriana Cali DECC Cali Colombia

concurrent constraint programming (ccp) is a model for concurrency where agents interact with each other by telling and asking constraints (i. e., formulas in logic) into a shared store of partial information. The ntcc calculus extends ccp with the notion of discrete time-units for the specification of reactive systems. Moreover, ntcc features constructors for non-deterministic choices and asynchronous behavior, thus allowing for (1) synchronization of processes via constraint entailment during a time-unit and (2) synchronization of processes along time-intervals. In this paper we develop the techniques needed for the automatic verification of ntcc programs based on symbolic model checking. We show that the internal transition relation, modeling the behavior of processes during a time-unit (1 above), can be symbolically represented by formulas in a suitable fragment of linear time temporal logic. Moreover, by using standard techniques as difference decision diagrams, we provide a compact representation of these constraints. Then, relying on a fixpoint characterization of the timed constructs, we obtain a symbolic model of the observable transition (2 above). We prove that our construction is correct with respect to the operational semantics. Finally, we introduce a prototypical tool implementing our method.

关键词： concurrent constraint programming temporal logic model checking

来源：评论

学校读者我要写书评

暂无评论

Proving concurrent constraint programming Correct, Revisited

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2015年 312卷 179-195页

作者： Olarte, Carlos Pimentel, Elaine Univ Fed Rio Grande do Norte ECT BR-59072970 Natal RN Brazil Pontificia Univ Javeriana Cali DECC Cali Colombia Univ Fed Rio Grande do Norte DMAT BR-59072970 Natal RN Brazil

concurrent constraint programming (CCP) is a simple and powerful model of concurrency where processes interact by telling and asking constraints into a global store of partial information. Since its inception, CCP has been endowed with declarative semantics where processes are interpreted as formulas in a given logic. This allows for the use of logical machinery to reason about the behavior of programs and to prove properties in a declarative way. Nevertheless, the logical characterization of CCP programs exhibits normally a weak level of adequacy since proofs in the logical system may not correspond directly to traces of the program. In this paper, relying on a focusing discipline, we show that it is possible to give a logical characterization to different CCP-based languages with the highest level of adequacy. We shall also provide a neater way of interpreting procedure calls by adding fixed points to the logical structure.

关键词： Linear Logic concurrent constraint programming Proof Systems Focusing Fixed Points

来源：评论

学校读者我要写书评

暂无评论

Dynamic Spaces in concurrent constraint programming

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2014年 305卷 103-121页

作者： Olarte, Carlos Nigam, Vivek Pimentel, Elaine Pontificia Univ Javeriana Cali Dept Elect & Ciencias Computac Cali Colombia Univ Fed Rio Grande Norte Natal Escola Ciencias & Tecnol Natal RN Brazil Univ Fed Paraiba Dept Informat Joao Pessoa Paraiba Brazil Univ Fed Minas Gerais Dept Matemat Belo Horizonte MG Brazil Univ Fed Rio Grande Norte Natal Natal RN Brazil

concurrent constraint programming (CCP) is a declarative model for concurrency where agents interact with each other by posting (telling) and asking constraints (formulas in logic) in a shared store of partial information. With the advent of emergent applications as security protocols, social networks and cloud computing, the CCP model has been extended in different directions to faithfully model such systems as follows: (1) It has been shown that a name-passing discipline, where agents can communicate local names, can be described through the interplay of local (there exists) processes along with universally (V) quantified asks. This strategy has been used, for instance, to model the generation and communication of fresh values (nonces) in mobile reactive systems as security protocols;and (2) the underlying constraint system in CCP has been enhanced with local stores for the specification of distributed spaces. Then, agents are allowed to share some information with others but keep some facts for themselves. Recently, we have shown that local stores can be neatly represented in CCP by considering a constraint system where constraints are built from a fragment of linear logic with subexponentials (SELL(sic)). In this paper, we explore the use of existential ((sic)) and universal ((sic)) quantification over subexponentials in SELL(sic) in order to endow CCP with the ability to communicate location (space) names. The resulting CCP language that we obtain is a model of distributed computation where it is possible to dynamically establish new shared spaces for communication. We thus extend the sort of mobility achieved in (1) -for variables - to dynamically change the shared spaces among agents - (2) above. Finally, we argue that the new CCP language can be used in the specification of service oriented computing systems.

关键词： concurrent constraint programming Linear Logic Subexponentials Mobility Distributed Spaces

来源：评论

学校读者我要写书评

暂无评论

A Proof Theoretic Study of Soft concurrent constraint programming

引用

THEORY AND PRACTICE OF LOGIC programming 2014年第4-5期14卷 649-663页

作者： Pimentel, Elaine Olarte, Carlos Nigam, Vivek Univ Fed Rio Grande do Norte BR-59072970 Natal RN Brazil Pontificia Univ Javeriana Cali Javeriana Colombia Univ Fed Paraiba BR-58059900 Joao Pessoa Paraiba Brazil

concurrent constraint programming (CCP) is a simple and powerful model for concurrency where agents interact by telling and asking constraints. Since their inception, CCP-languages have been designed for having a strong connection to logic. In fact, the underlying constraint system can be built from a suitable fragment of intuitionistic (linear) logic -ILL- and processes can be interpreted as formulas in ILL. constraints as ILL formulas fail to represent accurately situations where "preferences" (called soft constraints) such as probabilities, uncertainty or fuzziness are present. In order to circumvent this problem, c-semirings have been proposed as algebraic structures for defining constraint systems where agents are allowed to tell and ask soft constraints. Nevertheless, in this case, the tight connection to logic and proof theory is lost. In this work, we give a proof theoretical meaning to soft constraints: they can be defined as formulas in a suitable fragment of ILL with subexponentials (SELL) where subexponentials, ordered in a c-semiring structure, are interpreted as preferences. We hence achieve two goals: (1) obtain a CCP language where agents can tell and ask soft constraints and (2) prove that the language in (1) has a strong connection with logic. Hence we keep a declarative reading of processes as formulas while providing a logical framework for soft-CCP based systems. An interesting side effect of (1) is that one is also able to handle probabilities (and other modalities) in SELL, by restricting the use of the promotion rule for non-idempotent c-semirings. This finer way of controlling subexponentials allows for considering more interesting spaces and restrictions, and it opens the possibility of specifying more challenging computational systems.

关键词： concurrent constraint programming Linear Logic Soft constraints

来源：评论

学校读者我要写书评

暂无评论

A Proof Theoretic Study of Soft concurrent constraint programming

A Proof Theoretic Study of Soft Concurrent Constraint Progra...

引用

30th International Conference on Logic programming

关键词： concurrent constraint programming Linear Logic Soft constraints

来源：评论

学校读者我要写书评

暂无评论

Models and emerging trends of concurrent constraint programming

引用

constraintS 2013年第4期18卷 535-578页

作者： Olarte, Carlos Rueda, Camilo Valencia, Frank D. Pontificia Univ Javeriana Cali Dept Elect & Ciencias Comp Calle 18 118-250 Av Canasgordas Cali Colombia Ecole Polytech LIX CNRS F-91120 Palaiseau France

concurrent constraint programming (CCP) has been used over the last two decades as an elegant and expressive model for concurrent systems. It models systems of agents communicating by posting and querying partial information, represented as constraints over the variables of the system. This covers a vast variety of systems as those arising in biological phenomena, reactive systems, net-centric computing and the advent of social networks and cloud computing. In this paper we survey the main applications, developments and current trends of CCP.

关键词： concurrent constraint programming Concurrency Specification Verification

来源：评论

学校读者我要写书评

暂无评论

Dynamic Slicing for concurrent constraint Languages

引用

FUNDAMENTA INFORMATICAE 2020年第3-4期177卷 331-357页

作者： Falaschi, Moreno Gabbrielli, Maurizio Olarte, Carlos Palamidessi, Catuscia Univ Siena Dept Informat Engn & Math Siena Italy Univ Bologna Dipartimento Informat Sci & Ingn Bologna Italy Univ Fed Rio Grande do Norte ECT Escola Ciencias & Tecnol Natal RN Brazil Ecole Polytech INRIA Palaiseau France Ecole Polytech LIX Palaiseau France

concurrent constraint programming (CCP) is a declarative model for concurrency where agents interact by telling and asking constraints (pieces of information) in a shared store. Some previous works have developed (approximated) declarative debuggers for CCP languages. However, the task of debugging concurrent programs remains difficult. In this paper we define a dynamic slicer for CCP (and other language variants) and we show it to be a useful companion tool for the existing debugging techniques. We start with a partial computation (a trace) that shows the presence of bugs. Often, the quantity of information in such a trace is overwhelming, and the user gets easily lost, since she cannot focus on the sources of the bugs. Our slicer allows for marking part of the state of the computation and assists the user to eliminate most of the redundant information in order to highlight the errors. We show that this technique can be tailored to several variants of CCP, such as the timed language nt cc, linear CCP (an extension of CCP-based on linear logic where constraints can be consumed) and some extensions of CCP dealing with epistemic and spatial information. We also develop a prototypical implementation freely available for making experiments.

关键词： concurrent constraint programming Program slicing Debugging

来源：评论

学校读者我要写书评

暂无评论

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

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：