Showing 1–22 of 22 results for author: Olarte, C

Reasoning About Group Polarization: From Semantic Games to Sequent Systems

Authors: Robert Freiman, Carlos Olarte, Elaine Pimentel, Christian G. Fermüller

Abstract: Group polarization, the phenomenon where individuals become more extreme after interacting, has been gaining attention, especially with the rise of social media sha** people's opinions. Recent interest has emerged in formal reasoning about group polarization using logical systems. In this work we consider the modal logic PNL that captures the notion of agents agreeing or disagreeing on a given t… ▽ More Group polarization, the phenomenon where individuals become more extreme after interacting, has been gaining attention, especially with the rise of social media sha** people's opinions. Recent interest has emerged in formal reasoning about group polarization using logical systems. In this work we consider the modal logic PNL that captures the notion of agents agreeing or disagreeing on a given topic. Our contribution involves enhancing PNL with advanced formal reasoning techniques, instead of relying on axiomatic systems for analyzing group polarization. To achieve this, we introduce a semantic game tailored for (hybrid) extensions of PNL. This game fosters dynamic reasoning about concrete network models, aligning with our goal of strengthening PNL's effectiveness in studying group polarization. We show how this semantic game leads to a provability game by systemically exploring the truth in all models. This leads to the first cut-free sequent systems for some variants of PNL. Using polarization of formulas, the proposed calculi can be modularly adapted to consider different frame properties of the underlying model. △ Less

Submitted 2 May, 2024; originally announced May 2024.

Multi-modalities and non-commutativity/associativity in functorial linear logic: a case study

Authors: Carlos Olarte, Elaine Pimentel

Abstract: Similar to modal connectives, the exponential ! in intuitionistic linear logic (ILL) is not canonical, in the sense that if $i\not= j$ then $!^i F\not\equiv !^j F$. Intuitively, this means that we can mark the exponential with labels taken from a set I organized in a pre-order $\preceq$, obtaining (possibly infinitely-many) exponentials ($!^i$ for $i\in I$). There are, however, two main differen… ▽ More Similar to modal connectives, the exponential ! in intuitionistic linear logic (ILL) is not canonical, in the sense that if $i\not= j$ then $!^i F\not\equiv !^j F$. Intuitively, this means that we can mark the exponential with labels taken from a set I organized in a pre-order $\preceq$, obtaining (possibly infinitely-many) exponentials ($!^i$ for $i\in I$). There are, however, two main differences between multi-modalities in normal modal logics and subexponentials in linear logic. i. substructural behaviour. Subexponentials carry the possibility of having different structural behaviors; ii. nature of modalities. Normal modal logics start from the weakest version, assuming only axiom K, then extensions are considered, by adding other axioms. Exponentials in linear logic "take for granted" the behaviors expressed by axioms T and 4. Regarding (i), originally subexponentials could assume only weakening and contraction axioms, but later non-commutative/non-associative systems allowing commutative/ associative subexponentials were presented. Concerning (ii), Guerrini et al unified the modal and LL approaches, with the exponentials assuming only the linear version of K, with the possibility of adding modal extensions to it. This discussion was brought to multi-modal case, where subexponentials consider not only the structural axioms for contraction and weakening, but also the subexponential version of axioms {K,4,D,T}. In this work, we intend to join these two studies. This means that $!^{i}$ can behave classically or not, model associative and commutative systems or not, but also with exponential behaviors different from those in LL. Hence, by assigning different modal axioms one obtains, in a modular way, a class of different substructural modal logics. △ Less

Submitted 17 April, 2024; originally announced April 2024.

MSC Class: 03F52

Timed Strategies for Real-Time Rewrite Theories

Authors: Carlos Olarte, Peter Csaba Ölveczky

Abstract: In this paper we propose a language for conveniently defining a wide range of execution strategies for real-time rewrite theories, and provide Maude-strategy-implemented versions of most Real-Time Maude analysis methods, albeit with user-defined discrete and timed strategies. We also identify a new time sampling strategy that should provide both efficient and exhaustive analysis for many distribut… ▽ More In this paper we propose a language for conveniently defining a wide range of execution strategies for real-time rewrite theories, and provide Maude-strategy-implemented versions of most Real-Time Maude analysis methods, albeit with user-defined discrete and timed strategies. We also identify a new time sampling strategy that should provide both efficient and exhaustive analysis for many distributed real-time systems. We exemplify the use of our language and its analyses on a simple round trip time protocol, and compare the performance of standard Maude search with our strategy-implemented reachability analyses on the CASH scheduling algorithm benchmark. △ Less

Submitted 13 March, 2024; originally announced March 2024.

Unified Opinion Dynamic Modeling as Concurrent Set Relations in Rewriting Logic

Authors: Carlos Olarte, Carlos Ramírez, Camilo Rocha, Frank Valencia

Abstract: Social media platforms have played a key role in weaponizing the polarization of social, political, and democratic processes. This is, mainly, because they are a medium for opinion formation. Opinion dynamic models are a tool for understanding the role of specific social factors on the acceptance/rejection of opinions because they can be used to analyze certain assumptions on human behaviors. This… ▽ More Social media platforms have played a key role in weaponizing the polarization of social, political, and democratic processes. This is, mainly, because they are a medium for opinion formation. Opinion dynamic models are a tool for understanding the role of specific social factors on the acceptance/rejection of opinions because they can be used to analyze certain assumptions on human behaviors. This work presents a framework that uses concurrent set relations as the formal basis to specify, simulate, and analyze social interaction systems with dynamic opinion models. Standard models for social learning are obtained as particular instances of the proposed framework. It has been implemented in the Maude system as a fully executable rewrite theory that can be used to better understand how opinions of a system of agents can be shaped. This paper also reports an initial exploration in Maude on the use of reachability analysis, probabilistic simulation, and statistical model checking of important properties related to opinion dynamic models. △ Less

Submitted 14 February, 2024; originally announced February 2024.

A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets

Authors: Jaime Arias, Kyungmin Bae, Carlos Olarte, Peter Csaba Ölveczky, Laure Petrucci

Abstract: This paper presents a concrete and a symbolic rewriting logic semantics for parametric time Petri nets with inhibitor arcs (PITPNs), a flexible model of timed systems where parameters are allowed in firing bounds. We prove that our semantics is bisimilar to the "standard" semantics of PITPNs. This allows us to use the rewriting logic tool Maude, combined with SMT solving, to provide sound and comp… ▽ More This paper presents a concrete and a symbolic rewriting logic semantics for parametric time Petri nets with inhibitor arcs (PITPNs), a flexible model of timed systems where parameters are allowed in firing bounds. We prove that our semantics is bisimilar to the "standard" semantics of PITPNs. This allows us to use the rewriting logic tool Maude, combined with SMT solving, to provide sound and complete formal analyses for PITPNs. We develop and implement a new general folding approach for symbolic reachability, so that Maude-with-SMT reachability analysis terminates whenever the parametric state-class graph of the PITPN is finite. Our work opens up the possibility of using the many formal analysis capabilities of Maude -- including full LTL model checking, analysis with user-defined analysis strategies, and even statistical model checking -- for such nets. We illustrate this by explaining how almost all formal analysis and parameter synthesis methods supported by the state-of-the-art PITPN tool Romeo can be performed using Maude with SMT. In addition, we also support analysis and parameter synthesis from parametric initial markings, as well as full LTL model checking and analysis with user-defined execution strategies. Experiments show that our methods outperform Romeo in many cases. △ Less

Submitted 5 April, 2024; v1 submitted 3 January, 2024; originally announced January 2024.

Comments: arXiv admin note: substantial text overlap with arXiv:2303.08929

Proceedings of the 18th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice

Authors: Alberto Ciaffaglione, Carlos Olarte

Abstract: Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two deca… ▽ More Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop brings together designers, implementors and practitioners to discuss various aspects im**ing on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process. △ Less

Submitted 16 November, 2023; originally announced November 2023.

Comments: This volume contains the proceedings of the workshop Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'23)

Journal ref: EPTCS 396, 2023

Optimal Scheduling of Agents in ADTrees: Specialised Algorithm and Declarative Models

Authors: Jaime Arias, Carlos Olarte, Laure Petrucci, Łukasz Maśko, Wojciech Penczek, Teofil Sidoruk

Abstract: Expressing attack-defence trees in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance, e.g. attack time, of strategies executed by opposing coalitions. Optimal scheduling of agents' actions, a non-trivial problem, is thus vital. We discuss associated caveats and propose an algorithm that syn… ▽ More Expressing attack-defence trees in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance, e.g. attack time, of strategies executed by opposing coalitions. Optimal scheduling of agents' actions, a non-trivial problem, is thus vital. We discuss associated caveats and propose an algorithm that synthesises such an assignment, targeting minimal attack time and using the minimal number of agents for a given attack-defence tree. We also investigate an alternative approach for the same problem using Rewriting Logic, starting with a simple and elegant declarative model, whose correctness (in terms of schedule's optimality) is self-evident. We then refine this specification, inspired by the design of our specialised algorithm, to obtain an efficient system that can be used as a playground to explore various aspects of attack-defence trees. We compare the two approaches on different benchmarks. △ Less

Submitted 19 October, 2023; v1 submitted 8 May, 2023; originally announced May 2023.

Comments: arXiv admin note: text overlap with arXiv:2101.06838

Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving

Authors: Jaime Arias, Kyungmin Bae, Carlos Olarte, Peter Csaba Ölveczky, Laure Petrucci, Fredrik Rømming

Abstract: Parametric time Petri nets with inhibitor arcs (PITPNs) support flexibility for timed systems by allowing parameters in firing bounds. In this paper we present and prove correct a concrete and a symbolic rewriting logic semantics for PITPNs. We show how this allows us to use Maude combined with SMT solving to provide sound and complete formal analyses for PITPNs. We develop a new general folding a… ▽ More Parametric time Petri nets with inhibitor arcs (PITPNs) support flexibility for timed systems by allowing parameters in firing bounds. In this paper we present and prove correct a concrete and a symbolic rewriting logic semantics for PITPNs. We show how this allows us to use Maude combined with SMT solving to provide sound and complete formal analyses for PITPNs. We develop a new general folding approach for symbolic reachability that terminates whenever the parametric state-class graph of the PITPN is finite. We explain how almost all formal analysis and parameter synthesis supported by the state-of-the-art PITPN tool Roméo can be done in Maude with SMT. In addition, we also support analysis and parameter synthesis from parametric initial markings, as well as full LTL model checking and analysis with user-defined execution strategies. Experiments on three benchmarks show that our methods outperform Roméo in many cases. △ Less

Submitted 15 March, 2023; originally announced March 2023.

A Rewriting Logic Semantics and Statistical Analysis for Probabilistic Event-B

Authors: Carlos Olarte, Camilo Rocha, Daniel Osorio

Abstract: Probabilistic specifications are fast gaining ground as a tool for statistical modeling of probabilistic systems. One of the main goals of formal methods in this domain is to ensure that specific behavior is present or absent in the system, up to a certain confidence threshold, regardless of the way it operates amid uncertain information. This paper presents a rewriting logic semantics for a proba… ▽ More Probabilistic specifications are fast gaining ground as a tool for statistical modeling of probabilistic systems. One of the main goals of formal methods in this domain is to ensure that specific behavior is present or absent in the system, up to a certain confidence threshold, regardless of the way it operates amid uncertain information. This paper presents a rewriting logic semantics for a probabilistic extension of Event-B, a proof-based formal method for discrete systems modeling. The proposed semantics adequately captures the three sources of probabilistic behavior, namely, probabilistic assignments, parameters, and concurrency. Hence, simulation and probabilistic temporal verification become automatically available for probabilistic Event-B models. The approach takes as input a probabilistic Event-B specification, and outputs a probabilistic rewrite theory that is fully executable in PMaude and can be statistically tested against quantitative metrics. The approach is illustrated with examples in the paper. △ Less

Submitted 12 June, 2022; originally announced June 2022.

A Subexponential View of Domains in Session Types

Authors: Daniele Nantes, Carlos Olarte, Daniel Ventura

Abstract: Linear logic (LL) has inspired the design of many computational systems, offering reasoning techniques built on top of its meta-theory. Since its inception, several connections between concurrent systems and LL have emerged from different perspectives. In the last decade, the seminal work of Caires and Pfenning showed that formulas in LL can be interpreted as session types and processes in the pi-… ▽ More Linear logic (LL) has inspired the design of many computational systems, offering reasoning techniques built on top of its meta-theory. Since its inception, several connections between concurrent systems and LL have emerged from different perspectives. In the last decade, the seminal work of Caires and Pfenning showed that formulas in LL can be interpreted as session types and processes in the pi-calculus as proof terms. This leads to a Curry-Howard interpretation where proof reductions in the cut-elimination procedure correspond to process reductions/interactions. The subexponentials in LL have also played an important role in concurrent systems since they can be interpreted in different ways, including timed, spatial and even epistemic modalities in distributed systems. In this paper we address the question: What is the meaning of the subexponentials from the point of view of a session type interpretation? Our answer is a pi-like process calculus where agents reside in locations/sites and they make it explicit how the communication among the different sites should happen. The design of this language relies completely on the proof theory of the subexponentials in LL, thus extending the Caires-Pfenning interpretation in an elegant way. △ Less

Submitted 8 April, 2022; v1 submitted 8 October, 2021; originally announced October 2021.

Comments: In Proceedings LSFA 2021, arXiv:2204.03415

Journal ref: EPTCS 357, 2022, pp. 93-111

A Rewriting Logic Approach to Specification, Proof-search, and Meta-proofs in Sequent Systems

Authors: Carlos Olarte, Elaine Pimentel, Camilo Rocha

Abstract: This paper develops an algorithmic-based approach for proving inductive properties of propositional sequent systems such as admissibility, invertibility, cut-elimination, and identity expansion. Although undecidable in general, these structural properties are crucial in proof theory because they can reduce the proof-search effort and further be used as scaffolding for obtaining other meta-results… ▽ More This paper develops an algorithmic-based approach for proving inductive properties of propositional sequent systems such as admissibility, invertibility, cut-elimination, and identity expansion. Although undecidable in general, these structural properties are crucial in proof theory because they can reduce the proof-search effort and further be used as scaffolding for obtaining other meta-results such as consistency. The algorithms -- which take advantage of the rewriting logic meta-logical framework, and use rewrite- and narrowing-based reasoning -- are explained in detail and illustrated with examples throughout the paper. They have been fully mechanized in the L-Framework, thus offering both a formal specification language and off-the-shelf mechanization of the proof-search algorithms coming together with semi-decision procedures for proving theorems and meta-theorems of the object system. As illustrated with case studies in the paper, the L-Framework, achieves a great degree of automation when used on several propositional sequent systems, including single conclusion and multi-conclusion intuitionistic logic, classical logic, classical linear logic and its dyadic system, intuitionistic linear logic, and normal modal logics. △ Less

Submitted 8 January, 2021; originally announced January 2021.

A Semantic Framework for PEGs

Authors: Sérgio Medeiros, Carlos Olarte

Abstract: Parsing Expression Grammars (PEGs) are a recognition-based formalism which allows to describe the syntactical and the lexical elements of a language. The main difference between Context-Free Grammars (CFGs) and PEGs relies on the interpretation of the choice operator: while the CFGs' unordered choice e | e' is interpreted as the union of the languages recognized by e and e, the PEGs' prioritized c… ▽ More Parsing Expression Grammars (PEGs) are a recognition-based formalism which allows to describe the syntactical and the lexical elements of a language. The main difference between Context-Free Grammars (CFGs) and PEGs relies on the interpretation of the choice operator: while the CFGs' unordered choice e | e' is interpreted as the union of the languages recognized by e and e, the PEGs' prioritized choice e/e' discards e' if e succeeds. Such subtle, but important difference, changes the language recognized and yields more efficient parsing algorithms. This paper proposes a rewriting logic semantics for PEGs. We start with a rewrite theory giving meaning to the usual constructs in PEGs. Later, we show that cuts, a mechanism for controlling backtracks in PEGs, finds also a natural representation in our framework. We generalize such mechanism, allowing for both local and global cuts with a precise, unified and formal semantics. Hence, our work strives at better understanding and controlling backtracks in parsers for PEGs. The semantics we propose is executable and, besides being a parser with modest efficiency, it can be used as a playground to test different optimization ideas. More importantly, it is a mathematical tool that can be used for different analyses. △ Less

Submitted 9 November, 2020; originally announced November 2020.

ACM Class: F.4.2; F.4.3; D.3.4

Computational Logic for Biomedicine and Neurosciences

Authors: Elisabetta de Maria, Joelle Despeyroux, Amy Felty, Pietro Liò, Carlos Olarte, Abdorrahim Bahrami

Abstract: We advocate here the use of computational logic for systems biology, as a \emph{unified and safe} framework well suited for both modeling the dynamic behaviour of biological systems, expressing properties of them, and verifying these properties. The potential candidate logics should have a traditional proof theoretic pedigree (including either induction, or a sequent calculus presentation enjoying… ▽ More We advocate here the use of computational logic for systems biology, as a \emph{unified and safe} framework well suited for both modeling the dynamic behaviour of biological systems, expressing properties of them, and verifying these properties. The potential candidate logics should have a traditional proof theoretic pedigree (including either induction, or a sequent calculus presentation enjoying cut-elimination and focusing), and should come with certified proof tools. Beyond providing a reliable framework, this allows the correct encodings of our biological systems. % For systems biology in general and biomedicine in particular, we have so far, for the modeling part, three candidate logics: all based on linear logic. The studied properties and their proofs are formalized in a very expressive (non linear) inductive logic: the Calculus of Inductive Constructions (CIC). The examples we have considered so far are relatively simple ones; however, all coming with formal semi-automatic proofs in the Coq system, which implements CIC. In neuroscience, we are directly using CIC and Coq, to model neurons and some simple neuronal circuits and prove some of their dynamic properties. % In biomedicine, the study of multi omic pathway interactions, together with clinical and electronic health record data should help in drug discovery and disease diagnosis. Future work includes using more automatic provers. This should enable us to specify and study more realistic examples, and in the long term to provide a system for disease diagnosis and therapy prognosis. △ Less

Submitted 6 October, 2020; v1 submitted 15 July, 2020; originally announced July 2020.

A Game Model for Proofs with Costs

Authors: Timo Lang, Carlos Olarte, Elaine Pimentel, Christian Fermuller

Abstract: We look at substructural calculi from a game semantic point of view, guided by certain intuitions about resource conscious and, more specifically, cost conscious reasoning. To this aim, we start with a game, where player I defends a claim corresponding to a (single-conclusion) sequent, while player II tries to refute that claim. Branching rules for additive connectives are modeled by choices of II… ▽ More We look at substructural calculi from a game semantic point of view, guided by certain intuitions about resource conscious and, more specifically, cost conscious reasoning. To this aim, we start with a game, where player I defends a claim corresponding to a (single-conclusion) sequent, while player II tries to refute that claim. Branching rules for additive connectives are modeled by choices of II, while branching for multiplicative connectives leads to splitting the game into parallel subgames, all of which have to be won by player I to succeed. The game comes into full swing by adding cost labels to assumptions, and a corresponding budget. Different proofs of the same end-sequent are interpreted as more or less expensive strategies for I to defend the corresponding claim. This leads to a new kind of labelled calculus, which can be seen as a fragment of SELL (subexponential linear logic). Finally, we generalize the concept of costs in proofs by using a semiring structure, illustrate our interpretation by examples and investigate some proof-theoretical properties. △ Less

Submitted 27 June, 2019; originally announced June 2019.

Comments: To appear in TABLEAUX'19

The ILLTP Library for Intuitionistic Linear Logic

Authors: Carlos Olarte, Valeria de Paiva, Elaine Pimentel, Giselle Reis

Abstract: Benchmarking automated theorem proving (ATP) systems using standardized problem sets is a well-established method for measuring their performance. However, the availability of such libraries for non-classical logics is very limited. In this work we propose a library for benchmarking Girard's (propositional) intuitionistic linear logic. For a quick bootstrap** of the collection of problems, an… ▽ More Benchmarking automated theorem proving (ATP) systems using standardized problem sets is a well-established method for measuring their performance. However, the availability of such libraries for non-classical logics is very limited. In this work we propose a library for benchmarking Girard's (propositional) intuitionistic linear logic. For a quick bootstrap** of the collection of problems, and for discussing the selection of relevant problems and understanding their meaning as linear logic theorems, we use translations of the collection of Kleene's intuitionistic theorems in the traditional monograph "Introduction to Metamathematics". We analyze four different translations of intuitionistic logic into linear logic and compare their proofs using a linear logic based prover with focusing. In order to enhance the set of problems in our library, we apply the three provability-preserving translations to the propositional benchmarks in the ILTP Library. Finally, we generate a comprehensive set of reachability problems for Petri nets and encode such problems as linear logic sequents, thus enlarging our collection of problems. △ Less

Submitted 15 April, 2019; originally announced April 2019.

Comments: In Proceedings Linearity-TLLA 2018, arXiv:1904.06159

Journal ref: EPTCS 292, 2019, pp. 118-132

An Assertion language for slicing Constraint Logic Languages

Authors: Moreno Falaschi, Carlos Olarte

Abstract: Constraint Logic Programming (CLP) is a language scheme for combining two declarative paradigms: constraint solving and logic programming. Concurrent Constraint Programming (CCP) is a declarative model for concurrency where agents interact by telling and asking constraints in a shared store. In a previous paper, we developed a framework for dynamic slicing of CCP where the user first identifies th… ▽ More Constraint Logic Programming (CLP) is a language scheme for combining two declarative paradigms: constraint solving and logic programming. Concurrent Constraint Programming (CCP) is a declarative model for concurrency where agents interact by telling and asking constraints in a shared store. In a previous paper, we developed a framework for dynamic slicing of CCP where the user first identifies that a (partial) computation is wrong. Then, she marks (selects) some parts of the final state corresponding to the data (constraints) and processes that she wants to study more deeply. An automatic process of slicing begins, and the partial computation is "depurated" by removing irrelevant information. In this paper we give two major contributions. First, we extend the framework to CLP, thus generalizing the previous work. Second, we provide an assertion language suitable for both, CCP and CLP, which allows the user to specify some properties of the computations in her program. If a state in a computation does not satisfy an assertion then some "wrong" information is identified and an automatic slicing process can start. This way we make one step further towards automatizing the slicing process. We show that our framework can be integrated with the previous semi-automatic one, giving the user more choices and flexibility. We show by means of examples and experiments the usefulness of our approach. △ Less

Submitted 30 November, 2018; v1 submitted 14 August, 2018; originally announced August 2018.

Comments: Pre-proceedings paper presented at the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2018), Frankfurt am Main, Germany, 4-6 September 2018 (arXiv:1808.03326)

Report number: LOPSTR/2018/12

A Concurrent Constraint Programming Interpretation of Access Permissions

Authors: Carlos Olarte, Elaine Pimentel, Camilo Rueda

Abstract: A recent trend in object oriented (OO) 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… ▽ More A recent trend in object oriented (OO) 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 (lcc). 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 lcc 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 lcc 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 lcc 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. This paper is under consideration for publication in Theory and Practice of Logic Programming (TPLP). △ Less

Submitted 13 February, 2018; originally announced February 2018.

Comments: This paper is under consideration for publication in Theory and Practice of Logic Programming (TPLP)

Hybrid and Subexponential Linear Logics Technical Report

Authors: Joëlle Despeyroux, Carlos Olarte, Elaine Pimentel

Abstract: HyLL (Hybrid Linear Logic) and SELL (Subexponential Linear Logic) are logical frameworks that have been extensively used for specifying systems that exhibit modalities such as temporal or spatial ones. Both frameworks have linear logic (LL) as a common ground and they admit (cut-free) complete focused proof systems. The difference between the two logics relies on the way modalities are handled. In… ▽ More HyLL (Hybrid Linear Logic) and SELL (Subexponential Linear Logic) are logical frameworks that have been extensively used for specifying systems that exhibit modalities such as temporal or spatial ones. Both frameworks have linear logic (LL) as a common ground and they admit (cut-free) complete focused proof systems. The difference between the two logics relies on the way modalities are handled. In HyLL, truth judgments are labelled by worlds and hybrid connectives relate worlds with formulas. In SELL, the linear logic exponentials (!, ?) are decorated with labels representing locations, and an ordering on such labels defines the provability relation among resources in those locations. It is well known that SELL, as a logical framework, is strictly more expressive than LL. However, so far, it was not clear whether HyLL is more expressive than LL and/or SELL. In this paper, we show an encoding of the HyLL's logical rules into LL with the highest level of adequacy, hence showing that HyLL is as expressive as LL. We also propose an encoding of HyLL into SELL $\doublecup$ (SELL plus quantification over locations) that gives better insights about the meaning of worlds in HyLL. We conclude our expressiveness study by showing that previous attempts of encoding Computational Tree Logic (CTL) operators into HyLL cannot be extended to consider the whole set of temporal connectives. We show that a system of LL with fixed points is indeed needed to faithfully encode the behavior of such temporal operators. △ Less

Submitted 2 September, 2016; v1 submitted 31 August, 2016; originally announced August 2016.

Slicing Concurrent Constraint Programs

Authors: Moreno Falaschi, Maurizio Gabbrielli, Carlos Olarte, Catuscia Palamidessi

Abstract: 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 we show… ▽ More 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 we show it to be a useful companion tool for the existing debugging techniques. Our technique starts by considering 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 timed variants of CCP. We also develop a prototypical implementation freely available for making experiments. △ Less

Submitted 10 February, 2017; v1 submitted 18 August, 2016; originally announced August 2016.

Comments: Pre-proceedings paper presented at the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), Edinburgh, Scotland UK, 6-8 September 2016 (arXiv:1608.02534)

Report number: LOPSTR/2016/21

A Proof Theoretic Study of Soft Concurrent Constraint Programming

Authors: Elaine Pimentel, Carlos Olarte, Vivek Nigam

Abstract: 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 fo… ▽ More 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 interpretation 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. △ Less

Submitted 9 May, 2014; originally announced May 2014.

ACM Class: F.3.1; D.3.2

Journal ref: Theory and Practice of Logic Programming 14 (2014) 649-663

Abstract Interpretation of Temporal Concurrent Constraint Programs

Authors: Moreno Falaschi, Carlos Olarte, Catuscia Palamidessi

Abstract: 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 secu… ▽ More 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 a general framework for data flow analyses of tcc and utcc programs by abstract interpretation techniques. The concrete and abstract semantics 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 make also 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. △ Less

Submitted 9 December, 2013; originally announced December 2013.

ACM Class: F.3.1; D.3.2

Journal ref: Theory and Practice of Logic Programming 15 (2015) 312-357

Towards a Unified Framework for Declarative Structured Communications

Authors: Hugo A. López, Carlos Olarte, Jorge A. Pérez

Abstract: We present a unified framework for the declarative analysis of structured communications. By relying on a (timed) concurrent constraint programming language, we show that in addition to the usual operational techniques from process calculi, the analysis of structured communications can elegantly exploit logic-based reasoning techniques. We introduce a declarative interpretation of the language f… ▽ More We present a unified framework for the declarative analysis of structured communications. By relying on a (timed) concurrent constraint programming language, we show that in addition to the usual operational techniques from process calculi, the analysis of structured communications can elegantly exploit logic-based reasoning techniques. We introduce a declarative interpretation of the language for structured communications proposed by Honda, Vasconcelos, and Kubo. Distinguishing features of our approach are: the possibility of including partial information (constraints) in the session model; the use of explicit time for reasoning about session duration and expiration; a tight correspondence with logic, which formally relates session execution and linear-time temporal logic formulas. △ Less

Submitted 4 February, 2010; originally announced February 2010.

ACM Class: F.3.1; F.3.2; C.2.4

Journal ref: EPTCS 17, 2010, pp. 1-15