Navegando por Autor "Vega, Carlos Alberto Olarte"

Agora exibindo 1 - 20 de 20

Abstract interpretation of temporal concurrent constraint programs
(Cambridge University Press, 2014) Falaschi, Moreno; Palamidessi, Catuscia; Vega, Carlos Alberto Olarte
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
CI-posets, domínios e espaços de funções
(2019-11-25) Abdala, Jarafe Augusto; Santana, Fagner Lemos de; ; ; Vega, Carlos Alberto Olarte; ; Olguin, Cláudio Andres Callejas; ; Pimentel, Elaine Gouvea;
Considera-se posets (conjuntos parcialmente ordenados) que não são necessariamente contínuos tais que os seus intervalos com a ordem induzida constituem, por sua vez, posets contínuos. Associando-se à topologia de Scott, esta classe de posets desempenha um papel muito importante quando o interesse é caracterizar, de certa forma, o espaço das funções contínuas. Neste trabalho, o estudo é focado nas três topologias de Scott hereditárias, nomeadamente, hereditária para baixo, hereditária para cima e fracamente hereditária para cima, procurando-se caracterizar o espaço das funções contínuas definidas de um espaço core compacto X em um poset P, este último equipado com uma topologia de Scott hereditária e satisfazendo outras condições.
Dynamic spaces in concurrent constraint programming
(Elsevier, 2014) Nigam, Vivek; Pimentel, Elaine Gouvea; Vega, Carlos Alberto Olarte
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 (∃) processes along with universally (∀) 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). In this paper, we explore the use of existential (⋓) and universal (⋒) quantification over subexponentials in SELL 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
Especificação e verificação de protocolos de votação em lógica linear com focusing
(2018-05-28) Silva, Washington Cavalcante da; Vega, Carlos Alberto Olarte; ; ; Pimentel, Elaine Gouvea; ; Reis, Giselle Machado Nogueira;
A lógica linear (LL) tem se consolidado como um bom arcabouço para especificar sistemas computacionais, uma vez que fórmulas podem ser interpretadas como recursos que podem ser consumidos e/ou produzidos. Além disso, do ponto de vista da Teoria da Prova, a LL reconcilia o aspecto construtivo da lógica intuicionista com a simetria da lógica clássica. Desta maneira, é possível, de uma forma mais flexível, modelar estados de um sistema como fórmulas lógicas, e as transições entre esses estados como etapas na construção de uma prova. No entanto, a busca por provas, em geral, não é determinística, pois existem diferentes maneiras de se provar a mesma proposição. Visando reduzir esse problema, um sistema de provas focado pode ser utilizado nesse processo de busca. A grosso modo, um sistema focado considera provas em forma normal, reduzindo assim as ocorrências de provas não essenciais que são sintaticamente diferentes, mas equivalentes no final do processo. Neste trabalho, é apresentada a prova da completude de um sistema focado para a LL, bem como outras propriedades essenciais desse sistema. Além disso, o sistema focado será utilizado para especificar e verificar protocolos de votação, que definem como deve ser escolhido um candidato, feita uma contagem de votos, e divulgado o resultado de uma eleição. Para que isso seja possível, dois protocolos de votação serão especificados formalmente utilizando sistemas de transição de estados, que modelam de forma natural os estados e comportamento de tais protocolos. Junto a isso, para cada sistema, uma especificação em LL será definida e demonstrada que é correta, ou seja, que um passo focado representa uma determinada transição no sistema de estados modelado. Por fim, propriedades inerentes aos protocolos de votação, como a garantia de que o resultado da eleição reflete o desejo dos eleitores, serão apresentadas e demonstradas através de derivações no sistema focado.
Um estudo de lógica linear com subexponenciais
(2017-02-15) Orto, Laura Fernandes Dell; Vega, Carlos Alberto Olarte; Pimentel, Elaine Gouvea; ; http://lattes.cnpq.br/3298246411086415; ; http://lattes.cnpq.br/1198550954813139; ; http://lattes.cnpq.br/7762552636864447; Alvim, Mário Sérgio Ferreira; ; http://lattes.cnpq.br/1397639761790594; Pimentel, Elaine Gouvea; ; http://lattes.cnpq.br/3298246411086415
Em Lógica Clássica, podemos utilizar as hipóteses um número indeterminado de vezes. Por exemplo, a prova de um teorema pode fazer uso do mesmo lema várias vezes. Porém, em sistemas físicos, químicos e computacionais a situação é diferente: um recurso não pode ser reutilizado após ser consumido em uma ação. Em Lógica Linear, fórmulas são vistas como recursos a serem utilizados durante a prova. É essa noção de recursos que faz a Lógica Linear ser interessante para a modelagem de sistemas. Para tanto, a Lógica Linear controla o uso da contração e do enfraquecimento através dos exponenciais ! e ?. Este trabalho tem como objetivo fazer um estudo sobre a Lógica Linear com Subexponenciais (SELL), que é um refinamento da Lógica Linear. Em SELL, os exponenciais da Lógica Linear possuem índices, isto é, ! e ? serão substituídos por !i e ?i, onde “i” é um índice. Um dos pontos fundamentais de Teoria da Prova é a prova da Eliminação do Corte, que neste trabalho é demonstrada tanto para Lógica Linear como para SELL, onde apresentamos detalhes que normalmente são omitidos. A partir do teorema de Eliminação do Corte, podemos concluir a consistência do sistema (para as lógicas que estamos utilizando) e outros resultados como a propriedade de subfórmula. O trabalho inicia-se com um capítulo de Teoria da Prova, e em seguida se faz uma exposição sobre a Lógica Linear. Assim, com essas bases, apresenta-se a Lógica Linear com Subexponenciais. SELL tem sido utilizada, por exemplo, na especificação e verificação de diferentes sistemas tais como sistemas bioquímicos, sistemas de interação multimídia e, em geral, em sistemas concorrentes com modalidades temporais, espaciais e epistêmicas. Com essa base teórica bastante clara, apresenta-se a especificação de um sistema bioquímico utilizando SELL. Além disso, apresentamos várias instâncias de SELL que tem interpretações interessantes do ponto de vista computacional.
Formalização da lógica linear em Coq
(2017-02-15) Xavier, Bruno Francisco; Vega, Carlos Alberto Olarte; ; http://lattes.cnpq.br/1198550954813139; ; http://lattes.cnpq.br/0730802486637527; Pimentel, Elaine Gouvea; ; http://lattes.cnpq.br/3298246411086415; Alvim, Mário Sérgio Ferreira; ; http://lattes.cnpq.br/1397639761790594
Em teoria da prova, o teorema da eliminação do corte (ou Hauptsatz, que significa resultado principal) é de suma importância, uma vez que, em geral, implica na consistência e na propriedade subfórmula para um dado sistema. Ele assinala que qualquer prova em cálculo de sequentes que faz uso da regra do corte pode ser substituída por outra que não a utiliza. A prova procede por indução na ordem lexicográfica (peso da fórmula, altura do corte) e gera múltiplos casos quando a fórmula de corte é ou não principal. De forma geral, deve-se considerar a última regra aplicada nas duas premissas imediatamente depois de aplicar a regra do corte, o que gera um número considerável de situações. Por essa razão, a demonstração poderia ser propensa a erros na hipótese de recorremos a uma prova informal. A lógica linear (LL) é uma das lógicas subestruturais mais significativas e a regra do corte é admissível no seu cálculo de sequentes. Ela é um refinamento do modelo clássico e intuicionista. Sendo uma lógica sensível ao uso de recursos, LL tem sido amplamente utilizada na especificação e verificação de sistemas computacionais. À vista disso, se torna relevante sua abordagem neste trabalho. Nesta dissertação, formalizamos, em Coq, três cálculos de sequentes para a lógica linear e provamos que são equivalentes. Além disso, provamos metateoremas tais como admissibilidade da regra do corte, generalização das regras para axioma inicial, ! e copy e invertibilidade das regras para os conectivos 􀀀, ?, & e ?. No tocante à invertibilidade, demonstramos uma versão por indução sobre a altura da derivação e outra com aplicação da regra do corte, o que nos possibilitou conferir que, em um sistema que satisfaz Hauptsatz, a regra do corte simplifica bastante as provas em seu cálculo de sequentes. Com a finalidade de atenuar o número dos diversos casos, desenvolvemos várias táticas em Coq que nos permite realizar operações semiautomáticas.
From cut-free calculi to automated deduction: the case of bounded contraction
(Elsevier, 2017) Ciabattoni, Agata; Lellmann, Bjorn; Vega, Carlos Alberto Olarte; Pimentel, Elaine Gouvea
The addition of the bounded contraction rules to Full Lambek Calculus with exchange and weakening (FLew) gives rise to serious complications for proof search. For example, adding to FLew a naive version of these rules brakes cut-admissibility. Although this can be avoided by refining these rules, in this work we show that even “good” proof systems for FLew plus bounded contraction do not necessarily lead to good implementations. In order to solve this problem, we propose an extension of the lazy splitting methodology to bounded contractions, showing how to transform our focused, cut-free sequent calculus into a terminating theorem prover. Our system is used to show that the decision problem for FLew with bounded contraction is in EXPTIME
Hybrid and subexponential linear logics
(Elsevier, 2017) Despeyroux, Joelle; Pimentel, Elaine Gouvea; Vega, Carlos Alberto Olarte
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 (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
Linear logic as a logical framework
(Universidade Federal do Rio Grande do Norte, 2023-05-19) Xavier, Bruno Francisco; Vega, Carlos Alberto Olarte; Pimentel, Elaine Gouvea; http://lattes.cnpq.br/1198550954813139; https://orcid.org/0000-0003-1574-1779; http://lattes.cnpq.br/0730802486637527; Reis, Giselle Machado Nogueira; Santiago, Regivan Hugo Nunes; http://lattes.cnpq.br/7536988783793885; Costa, Umberto Souza da
Esta tese investiga a analiticidade de sistemas de prova por meio da Lógica Linear (LL). A analiticidade é a propriedade de que uma prova de uma fórmula F usa apenas subfórmulas de F. No cálculo de sequentes, essa propriedade é geralmente estabelecida mostrando que a regra de corte é admissível, o que significa que a introdução do lema auxiliar A na proposição “se A segue de B e C segue de A, então C segue de B” pode ser eliminada. No entanto, a eliminação de corte é um processo complexo que envolve múltiplas transformações de prova e requer o uso de procedimentos (semi-)automáticos para evitar erros. LL é uma ferramenta poderosa para estudar a analiticidade de sistemas de prova devido à sua natureza orientada à recursos, ao sistema focado e seu teorema de eliminação de corte. Trabalhos anteriores de Miller e Pimentel utilizaram LL como um framework lógico para estabelecer condições suficientes para a eliminação de corte de lógicas objeto. No entanto, muitos sistemas lógicos não podem ser adequadamente codificados em LL, particularmente sistemas de sequentes para lógicas modais. Nesta tese, propomos um sistema de sequentes aninhados linearmente (LNS, do inglês linear nested sequents) de uma variante de LL com subexponenciais (MMLL) e demonstramos que é possível estabelecer um critério de eliminação de corte para uma classe mais ampla de sistemas lógicos. Isso inclui sistemas de prova LNS para lógicas multimodais clássicas e subestruturais, bem como o sistema LNS para lógica intuicionista. Além disso, apresentamos um estudo detalhado do procedimento de eliminação de corte para LL. Especificamente, propomos um conjunto de regras de corte para sistemas focados em LL, uma variante de LL com subexponenciais (SELL) e MMLL. Nossa pesquisa demonstrou que essas regras de corte são suficientes para estabelecer diretamente a admissibilidade de corte nos sistemas focados. Formalizamos nossos resultados em Coq, um assistente de prova formal, fornecendo procedimentos para verificar a eliminação de corte de vários sistemas lógicos que são comumente usados em filosofia, matemática e ciência da computação.
Mechanizing focused linear logic in coq
(Elsevier, 2018) Xavier, Bruno; Vega, Carlos Alberto Olarte; Reis, Giselle; Nigam, Vivek
Linear logic has been used as a foundation (and inspiration) for the development of programming languages, logical frameworks and models for concurrency. Linear logic's cut-elimination and the completeness of focusing are two of its fundamental properties that have been exploited in such applications. Cut-elimination guarantees that linear logic is consistent and has the so-called sub-formula property. Focusing is a discipline for proof search that was introduced to reduce the search space, but has proved to have more value, as it allows one to specify the shapes of proofs available. This paper formalizes first-order linear logic in Coq and mechanizes the proof of cut-elimination and the completeness of focusing. Moreover, the implemented logic is used to encode an object logic, such as in a linear logical framework, and prove adequacy
Modalities in ecumenical systems
(Universidade Federal do Rio Grande do Norte, 2020-10-27) Sales, Emerson Wendlingger Dantas; Pimentel, Elaine Gouvea; ; http://lattes.cnpq.br/3298246411086415; ; http://lattes.cnpq.br/6472462085685049; Santana, Fagner Lemos de; ; http://lattes.cnpq.br/9444112594388983; Vega, Carlos Alberto Olarte; ; http://lattes.cnpq.br/1198550954813139; Marin, Sônia; ; http://lattes.cnpq.br/8013808109008817; Pereira, Luiz Carlos Dias Pinheiro; ; http://lattes.cnpq.br/8418729116626386
A discussão sobre como reunir os sistemas de Gentzen para lógica clássica e intuicionista em um único sistema unificado está de volta à tona. Recentemente, Prawitz e outros têm discutido os chamados Sistemas Ecumênicos, onde conectivos dessas lógicas podem coexistir em paz. No sistema de Prawitz, o lógico clássico e o lógico intuicionista compartilhariam o quantificador universal, conjunção, negação e a constante para o absurdo, mas cada um teria seu próprio quantificador existencial, disjunção e implicação, com significados diferentes. A ideia principal de Prawitz é que esses diferentes significados são dados por uma estrutura semântica que pode ser aceita por ambas as partes. Em um trabalho recente, um cálculo sequencial ecumênico e um sistema aninhado foram apresentados, e algumas propriedades de teoria da prova muito interessantes dos sistemas foram estabelecidas. Neste trabalho, a noção de verdade na Lógica Ecumênica de Prawitz será estendida, de forma a definir modalidades aléticas ecumênicas.
Modelling non-Markovian dynamics in biochemical reactions
(BMC, 2015) Chiarugi, Davide; Falaschi, Moreno; Hermith, Diana; Vega, Carlos Alberto Olarte; Torella, Luca
Background Biochemical reactions are often modelled as discrete-state continuous-time stochastic processes evolving as memoryless Markov processes. However, in some cases, biochemical systems exhibit non-Markovian dynamics. We propose here a methodology for building stochastic simulation algorithms which model more precisely non-Markovian processes in some specific situations. Our methodology is based on Constraint Programming and is implemented by using Gecode, a state-of-the-art framework for constraint solving. Results Our technique allows us to randomly sample waiting times from probability density functions that not necessarily are distributed according to a negative exponential function. In this context, we discuss an important case-study in which the probability density function is inferred from single-molecule experiments that describe the distribution of the time intervals between two consecutive enzymatically catalysed reactions. Noticeably, this feature allows some types of enzyme reactions to be modelled as non-Markovian processes. Conclusions We show that our methodology makes it possible to obtain accurate models of enzymatic reactions that, in specific cases, fit experimental data better than the corresponding Markovian models
On concurrent behaviors and focusing in linear logic
(Elsevier, 2017) Vega, Carlos Alberto Olarte; Pimentel, Elaine Gouvea
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 of them. 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, we study different encodings from CCP into intuitionistic linear logic (ILL) and we compare the level of adequacy attained in each. By relying on a focusing discipline, we show that it is possible to give a logical characterization to CCP with the highest level of adequacy. Moreover, we show how to characterize maximal-parallelism semantics for CCP by relying on a multi-focusing discipline for ILL. These results, besides giving proof techniques for CCP, entail (safe) optimizations for the execution of CCP programs. Finally, we show how to interpret CCP procedure calls as fixed points in ILL, thus opening the possibility of reasoning by induction about properties of CCP programs
A proof theoretic study of soft concurrent constraint programming
(Cambridge University Press, 2014) Pimentel, Elaine Gouvea; Nigam, Vivek; Vega, Carlos Alberto Olarte
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
A proof theoretic view of spatial and temporal dependencies in biochemical systems
(Elsevier, 2016) Vega, Carlos Alberto Olarte; Chiarugi, Davide; Hermith, Diana; Falaschi, Moreno
The behavior of biochemical systems such as metabolic and signaling pathways may depend on either the location of the reactants or on the time needed for a reaction to occur. In this paper we propose a formalism for specifying and verifying properties of biochemical systems that combines, coherently, temporal and spatial modalities. To this aim, we consider a fragment of intuitionistic linear logic with subexponentials (SELL). The subexponential signature allows us to capture the spatial relations among the different components of the system and the timed constraints. We illustrate our approach by specifying some well-known biological systems and verifying properties of them. Moreover, we show that our framework is general enough to give a logic-based semantics to P systems. We show that the proposed logical characterizations have a strong level of adequacy. Hence, derivations in SELL follow exactly the behavior of the modeled system
Proving concurrent constraint programming correct, revisited
(Elsevier, 2015) Vega, Carlos Alberto Olarte; Pimentel, Elaine Gouvea
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
Subexponential concurrent constraint programming
(Elsevier, 2015) Pimentel, Elaine Gouvea; Nigam, Vivek; Vega, Carlos Alberto Olarte
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) 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
A Symbolic model for timed concurrent constraint programming
(Elsevier, 2015) Arias, Jaime; Guzman, Michell; Vega, Carlos Alberto Olarte
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
A uniform framework for substructural logics with modalities
(Easy Chair, 2017-05-04) Vega, Carlos Alberto Olarte; Lellmann, Björn; Pimentel, Elaine Gouvea
It is well known that context dependent logical rules can be problematic both to implement and reason about. This is one of the factors driving the quest for better behaved, i.e., local, logical systems. In this work we investigate such a local system for linear logic (LL) based on linear nested sequents (LNS). Relying on that system, we propose a general framework for modularly describing systems combining, coherently, substructural behaviors inherited from LL with simply dependent multimodalities. This class of systems includes linear, elementary, a ne, bounded and subexponential linear logics and extensions of multiplicative additive linear logic (MALL) with normal modalities, as well as general combinations of them. The resulting LNS systems can be adequately encoded into (plain) linear logic, supporting the idea that LL is, in fact, a “universal framework” for the specification of logical systems. From the theoretical point of view, we give a uniform presentation of LL featuring di erent axioms for its modal operators. From the practical point of view, our results lead to a generic way of constructing theorem provers for di erent logics, all of them based on the same grounds. This opens the possibility of using the same logical framework for reasoning about all such logical systems
Verification of spatial and temporal modalities in biochemical systems
(Elsevier, 2015) Falaschi, Moreno; Hermith, Diana; Chiarugi, Davide; Vega, Carlos Alberto Olarte
Biochemical systems such as metabolic and signaling pathways tend to be arranged in a physical space: the product of one reaction must be in the right place to become the reactant for the subsequent reaction in the pathway. Moreover, in some cases, the behavior of the systems can depend on both, the location of the reactants as well as on the time needed for the reaction to occur. We address the problem of specifying and verifying properties of biochemical systems that exhibit both temporal and spatial modalities at the same time. For that, we use as specification language a fragment of intuitionistic linear logic with subexponentials (SELL). The subexponential signature allows us to capture the spatial relations among the different components of the system and the timed constraints for reactions to occur. We show that our framework is general enough to give a declarative semantics to P-Systems and we show that such logical characterization has a strong level of adequacy. Hence, derivations in SELL follow exactly the behavior of the modeled system.

SIGAA

Navegando por Autor "Vega, Carlos Alberto Olarte"