Search

Your search keyword '"Bonchi, Filippo"' showing total 15 results
Start Over Author "Bonchi, Filippo" Topic [info.info-lo]computer science [cs]/logic in computer science [cs.lo]
15 results on '"Bonchi, Filippo"'

1. Presenting convex sets of probability distributions by convex semilattices and unique bases

Author

Bonchi, Filippo, Sokolova, Ana, Valeria, Vignudelli, University of Pisa - Università di Pisa, University of Salzburg, École normale supérieure de Lyon (ENS de Lyon), Centre National de la Recherche Scientifique (CNRS), Université Claude Bernard Lyon 1 (UCBL), Université de Lyon, Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), ANR-20-CE48-0005,QuaReMe,Méthodes de raisonnement quantitative pour les logiques probabilistiques(2020), ANR-16-CE25-0011,REPAS,Des systèmes logiciels fiables et conscients des données privées, via les métriques de bisimulation(2016), ANR-10-LABX-0070,MILYON,Community of mathematics and fundamental computer science in Lyon(2010), ANR-11-IDEX-0007,Avenir L.S.E.,PROJET AVENIR LYON SAINT-ETIENNE(2011), and European Project: 678157,H2020,ERC-2015-STG,CoVeCe(2016)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Convex semilattices, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Convex sets of distributions monad, Unique base, Logic in Computer Science (cs.LO)
Abstract

International audience; We prove that every finitely generated convex set of finitely supported probability distributions has a unique base. We apply this result to provide an alternative proof of a recent result: the algebraic theory of convex semilattices presents the monad of convex sets of probability distributions.

Published
2021

2. 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

Author

Bonchi, Filippo, König, Barbara, Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Universität Duisburg-Essen [Essen], Filippo Bonchi, Barbara Konig, Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), and Universität Duisburg-Essen = University of Duisburg-Essen [Essen]

Subjects
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], ComputingMilieux_MISCELLANEOUS
Abstract

International audience

Published
2019

3. Bialgebraic Semantics for Logic Programming

Author

Bonchi, Filippo, Zanasi, Fabio, Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), ANR-10-LABX-0070,MILYON,Community of mathematics and fundamental computer science in Lyon(2010), Bonchi F., Zanasi F., Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), and École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Pure mathematics, Bialgebrae, Trace (linear algebra), General Computer Science, Coalgebra, Pseudometric space, Coalgebrae on presheaves, Compositionality, Logic programming, Theoretical Computer Science, Computer Science (all), Measure (mathematics), Coalgebrae on presheave, Computer Science::Logic in Computer Science, Mathematics::Category Theory, ComputingMilieux_MISCELLANEOUS, Mathematics, Probability measure, Functor, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Order (ring theory), Logic in Computer Science (cs.LO), Distributive property, Computer Science::Programming Languages
Abstract

We study different behavioral metrics, such as those arising from both branching and linear-time semantics, in a coalgebraic setting. Given a coalgebra $\alpha\colon X \to HX$ for a functor $H \colon \mathrm{Set}\to \mathrm{Set}$, we define a framework for deriving pseudometrics on $X$ which measure the behavioral distance of states. A crucial step is the lifting of the functor $H$ on $\mathrm{Set}$ to a functor $\overline{H}$ on the category $\mathrm{PMet}$ of pseudometric spaces. We present two different approaches which can be viewed as generalizations of the Kantorovich and Wasserstein pseudometrics for probability measures. We show that the pseudometrics provided by the two approaches coincide on several natural examples, but in general they differ. If $H$ has a final coalgebra, every lifting $\overline{H}$ yields in a canonical way a behavioral distance which is usually branching-time, i.e., it generalizes bisimilarity. In order to model linear-time metrics (generalizing trace equivalences), we show sufficient conditions for lifting distributive laws and monads. These results enable us to employ the generalized powerset construction.

Published
2015

4. Towards Trace Metrics via Functor Lifting

Author

Baldan, Paolo, Bonchi, Filippo, Henning, Kerstan, König, Barbara, Dipartimento di Matematica [Padova], Universita degli Studi di Padova, Concurrency, Mobility and Transactions (COMETE), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), Universität Duisburg-Essen [Essen], ANR-10-LABX-0070,MILYON,Community of mathematics and fundamental computer science in Lyon(2010), Università degli Studi di Padova = University of Padua (Unipd), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), and Universität Duisburg-Essen = University of Duisburg-Essen [Essen]

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, 000 Computer science, knowledge, general works, Mathematics::Rings and Algebras, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Logic in Computer Science (cs.LO), Informatik, Coalgebra, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Monad lifting, Mathematics::K-Theory and Homology, Pseudometric, Trace metric, Software, Mathematics::Quantum Algebra, Computer Science::Logic in Computer Science, Mathematics::Category Theory, Computer Science, Mathematik
Abstract

International audience; We investigate the possibility of deriving metric trace semantics in a coalgebraic framework.First, we generalize a technique for systematically lifting functors from the category Set ofsets to the category PMet of pseudometric spaces, by identifying conditions under whichalso natural transformations, monads and distributive laws can be lifted. By exploiting somerecent work on an abstract determinization, these results enable the derivation of trace metricsstarting from coalgebras in Set. More precisely, for a coalgebra on Set we determinize it,thus obtaining a coalgebra in the Eilenberg-Moore category of a monad. When the monadcan be lifted to PMet, we can equip the final coalgebra with a behavioral distance. The tracedistance between two states of the original coalgebra is the distance between their images in thedeterminized coalgebra through the unit of the monad. We show how our framework appliesto nondeterministic automata and probabilistic automata.

Published
2015
Full Text
View/download PDF

5. Final Semantics for Decorated Traces

Author

Bonchi, Filippo, Bonsangue, Marcello, Rutten, Jan, Silva, Alexandra, Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Centrum voor Wiskunde en Informatica (CWI), Centrum Wiskunde & Informatica (CWI)-Netherlands Organisation for Scientific Research, École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), and Bonchi, Filippo

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

International audience; In concurrency theory, various semantic equivalences on labelled transition systems are based on traces enriched or decorated with some additional observations. They are generally referred to as decorated traces, and examples include ready, failure, trace and complete trace equivalence. Using the generalized powerset construction, recently introduced by a subset of the authors [13], we give a coalgebraic presentation of decorated trace semantics. This yields a uniform notion of canonical, minimal representatives for the various decorated trace equivalences, in terms of final Moore automata. As a consequence, proofs of decorated trace equivalence can be given by coinduction, using different types of (Moore-) bisimulation (up-to), which is helpful for automation.

Published
2012

6. Mathematical Structures in Computer Science Preface to special issue: EXPRESS, ICE and SOS 2009

Author

Bonchi, Filippo, Klin, Bartek, Fröschle, Sibylle B., Gorla, Daniele, Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Dipartimento di Informatica e Sistemistica 'Antonio Ruberti' (DIS), Università degli Studi di Roma 'La Sapienza' = Sapienza University [Rome], École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Università degli Studi di Roma 'La Sapienza' = Sapienza University [Rome] (UNIROMA), Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), and Université de Lyon-École normale supérieure - Lyon (ENS Lyon)

Subjects
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], ComputingMilieux_MISCELLANEOUS
Abstract

International audience

Published
2012

7. A Recursion-Theoretic Characterization of the Probabilistic Class PP

Author

Dal Lago, Ugo, Kahle, Reinhard, Oitavem, Isabel, Foundations of Component-based Ubiquitous Systems (FOCUS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Dipartimento di Informatica - Scienza e Ingegneria [Bologna] (DISI), Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO)-Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), Universidade Nova de Lisboa = NOVA University Lisbon (NOVA), Mathematisches Institut [Tübingen], Eberhard Karls Universität Tübingen = Eberhard Karls University of Tuebingen, F. Bonchi, S. J. Puglisi, Dal Lago U., Kahle R., Oitavem I., CMA - Centro de Matemática e Aplicações, DM - Departamento de Matemática, Bonchi, Filippo, and Puglisi, Simon J.

Subjects
probabilistic classes, Probabilistic classes, polynomial time, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Theory of computation → Recursive functions, Computer Science::Computational Complexity, Pp, PP, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Implicit complexity, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Polynomial time, Tree-recursion, tree-recursion, Software, Probabilistic classe
Abstract

Probabilistic complexity classes, despite capturing the notion of feasibility, have escaped any treatment by the tools of so-called implicit-complexity. Their inherently semantic nature is of course a barrier to the characterization of classes like BPP or ZPP, but not all classes are semantic. In this paper, we introduce a recursion-theoretic characterization of the probabilistic class PP, using recursion schemata with pointers., LIPIcs, Vol. 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), pages 35:1-35:12

Published
2021

8. A Categorical Semantics of Signal Flow Graphs

Author

Fabio Zanasi, Pawel Sobocinski, Filippo Bonchi, Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), ECS Department - University of Southampton, University of Southampton, École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), and Bonchi, Filippo

Subjects
Discrete mathematics, Polynomial, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], business.industry, Computer science, Computer Science (all), [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Pattern recognition, Categorical semantics, Field (mathematics), Theoretical Computer Science, Composition (combinatorics), Modular design, 16. Peace & justice, Distributive property, Artificial intelligence, business, Signal-flow graph
Abstract

International audience; We introduce IH, a sound and complete graphical theory of vector subspaces over the field of polynomial fractions, with relational composition. The theory is constructed in modular fashion, using Lack's approach to composing PROPs with distributive laws. We then view string diagrams of IH as generalised stream circuits by using a formal Laurent series semantics. We characterize the subtheory where circuits adhere to the classical notion of signal flow graphs, and illustrate the use of the graphical calculus on several examples.

Published
2014

9. Saturated Semantics for Coalgebraic Logic Programming

Author

Filippo Bonchi, Fabio Zanasi, Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), and Bonchi, Filippo

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Theoretical computer science, Programming language, Principle of compositionality, Process calculus, Coalgebra, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 0102 computer and information sciences, 02 engineering and technology, computer.software_genre, 01 natural sciences, Operational semantics, Action semantics, Denotational semantics, 010201 computation theory & mathematics, Well-founded semantics, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, computer, Logic programming, ComputingMilieux_MISCELLANEOUS, Mathematics
Abstract

A series of recent papers introduces a coalgebraic semantics for logic programming, where the behavior of a goal is represented by a parallel model of computation called coinductive tree. This semantics fails to be compositional, in the sense that the coalgebra formalizing such behavior does not commute with the substitutions that may apply to a goal. We suggest that this is an instance of a more general phenomenon, occurring in the setting of interactive systems (in particular, nominal process calculi), when one tries to model their semantics with coalgebrae on presheaves. In those cases, compositionality can be obtained through saturation. We apply the same approach to logic programming: the resulting semantics is compositional and enjoys an elegant formulation in terms of coalgebrae on presheaves and their right Kan extensions.

Published
2013

10. A Presheaf Environment for the Explicit Fusion Calculus

Author

Filippo Bonchi, Vincenzo Ciancia, Maria Grazia Buscemi, Fabio Gadducci, Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Institutions, Markets, Technologies (IMT), IMT Institute for Advanced Studies [Lucca], Dipartimento di Informatica [Pisa], University of Pisa - Università di Pisa, This work was carried out during the first author's tenure of an ERCIM 'Alain Bensoussan' Fellowship Programme. The third author has been supported by the Comunidad de Madrid program ProMeSaS (S-0505/TIC/0407) and by the Netherlands Organization for Scientific Research VICI grant 639.073.501. The fourth author has been partly supported by the Italian Ministry of University and Research project SisteR (PRIN 20088HXMYN)., Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), Bonchi, Filippo, and École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL)

Subjects
Pure mathematics, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Presheaf, 0102 computer and information sciences, 02 engineering and technology, Algebras, 01 natural sciences, Denotational semantics, Morphism, Artificial Intelligence, Mathematics::Category Theory, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Calculus, Equivalence relation, Nominal calculi, Equivalence (formal languages), Mathematics, Fusion, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Rotation formalisms in three dimensions, Injective function, Presheaf categories, Computational Theory and Mathematics, Coalgebras, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Programming Languages, 020201 artificial intelligence & image processing, Software
Abstract

Name passing calculi are nowadays one of the preferred formalisms for the specification of concurrent and distributed systems with a dynamically evolving topology. Despite their widespread adoption as a theoretical tool, though, they still face some unresolved semantic issues, since the standard operational, denotational and logical methods often proved inadequate to reason about these formalisms. A domain which has been successfully employed for languages with asymmetric communication, like the ?-calculus, are presheaf categories based on (injective) relabellings, such as $Set^{\mathbb{I}}$ . Calculi with symmetric binding, in the spirit of the fusion calculus, give rise to novel research challenges. In this work we examine the explicit fusion calculus, and propose to model its syntax and semantics using the presheaf category $Set^\mathbb{E}$ , where $\mathbb{E}$ is the category of equivalence relations and equivalence preserving morphisms.

Published
2012

11. Towards a General Theory of Barbs, Contexts and Labels

Author

Fabio Gadducci, Filippo Bonchi, Giacoma Valentina Monreale, Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Dipartimento di Informatica [Pisa], University of Pisa - Università di Pisa, Dipartimento di Informatica [Pisa] (DI), Springer, Bonchi, Filippo, Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), and École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL)

Subjects
Infinite set, Theoretical computer science, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Computer science, business.industry, 010102 general mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 0102 computer and information sciences, Semantics, 01 natural sciences, Operational semantics, Predicate (grammar), Formalism (philosophy of mathematics), General theory, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Artificial intelligence, 0101 mathematics, Equivalence (formal languages), business, Equivalence (measure theory)
Abstract

International audience; Barbed bisimilarity is a widely-used behavioural equivalence for interactive systems: given a set of predicates (denoted "barbs", and representing basic observations on states) and a set of contexts (representing the possible execution environments), two systems are deemed to be equivalent if they verify the same barbs whenever inserted inside any of the chosen contexts. Despite its flexibility, this definition of equivalence is unsatisfactory, since often the quantification is over an infinite set of contexts, thus making barbed bisimilarity very hard to be verified. Should a labelled operational semantics be available for our system, more efficient observational equivalences might be adopted. To this end, a series of techniques have been proposed to derive labelled transition systems (LTSs) from unlabelled ones, the main example being Leifer and Milner's reactive systems. The underlying intuition is that labels are the "minimal" contexts that allow for a reduction to be performed. We introduce a framework that characterizes (weak) barbed bisimilarity via transition systems whose labels are (possibly minimal) contexts. Differently from other proposals, our theory is not dependent on the way LTSs are built, and it relies on a simple set-theoretical presentation. To provide a test-bed for our formalism, we instantiate it by addressing the semantics of mobile ambients and HoCore, recasting the (weak) barbed bisimilarities of these calculi via label-based behavioural equivalences.

Published
2012

12. Brzozowski’s Algorithm (Co)Algebraically

Author

Bonchi, F., Bonsangue, M., Rutten, J., Silva, A., Constable, R., Laboratoire de l'Informatique du Parallélisme (LIP), Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), Centrum voor Wiskunde en Informatica (CWI), Centrum Wiskunde & Informatica (CWI)-Netherlands Organisation for Scientific Research, École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Constable, R., Silva, A., École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), and Bonchi, Filippo

Subjects
Discrete mathematics, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Correctness, Coalgebra, Data Science, Duality (mathematics), Computer Science (all), [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Theoretical Computer Science, Simple (abstract algebra), Deterministic automaton, Reachability, Universal algebra, Lecture Notes in Computer Science, Observability, Algorithm, Computer Science::Formal Languages and Automata Theory, Mathematics
Abstract

International audience; We give a new presentation of Brzozowski's algorithm to minimize finite automata, using elementary facts from universal algebra and coalgebra, and building on earlier work by Arbib and Manes on the duality between reachability and observability. This leads to a simple proof of its correctness and opens the door to further generalizations.

Published
2012

13. RPO Semantics for Mobile Ambients

Author

Fabio Gadducci, Filippo Bonchi, Giacoma Valentina Monreale, Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Dipartimento di Informatica [Pisa], University of Pisa - Università di Pisa, Dipartimento di Informatica [Pisa] (DI), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), and Bonchi, Filippo

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Theoretical computer science, Process calculus, Mechanism based, computer.software_genre, Operational semantics, Mathematics (miscellaneous), Ambient calculus, Borrowed contexts, Relative-pushouts, Ambient Calculus, Rule of inference, Labelled transition systems, Mathematics, Graph Rewriting, Graphic methods, Semantics, Borrowed contexts, Inference rules, Labelled transition systems, Mobile ambients, Operational semantics, Relative-pushouts, Structural congruences, Synthesis mechanism, Graph rewriting, Programming language, Testbed, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Graph, Semantics, Computer Science Applications, Graphic methods, Inference rules, Structural congruences, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Deriving Labeled Transition Systems, Synthesis mechanism, Mobile ambients, computer
Abstract

In this paper we focus on the synthesis of labelled transition systems (LTSs) for process calculi using Mobile Ambients (MAs) as a testbed. Our proposal is based on a graphical encoding: a process is mapped into a graph equipped with interfaces such that the denotation is fully abstract with respect to the standard structural congruence. Graphs with interfaces are amenable to the synthesis mechanism based on borrowed contexts (BCs), which is an instance of relative pushouts (RPOs). The BC mechanism allows the effective construction of an LTS that has graphs with interfaces as states and labels, and such that the associated bisimilarity is a congruence. We focus here on the analysis of an LTS over processes as graphs with interfaces: we use the LTS on graphs to recover an LTS directly defined over the structure of MA processes and define a set of SOS inference rules capturing the same operational semantics.

Published
2011

14. A lattice-theoretical perspective on adhesive categories

Author

Tobias Heindel, Paolo Baldan, Andrea Corradini, Filippo Bonchi, Barbara König, Bonchi, Filippo, Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Dipartimento di Informatica, University of Ca’ Foscari [Venice, Italy], Dipartimento di Informatica [Pisa] (DI), University of Pisa - Università di Pisa, Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA), Abteilung Informatik und angewandte Kognitionswissenschaft [Duisburg] (INKO), Universität Duisburg-Essen = University of Duisburg-Essen [Essen], École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Laboratoire d'Intégration des Systèmes et des Technologies (LIST), Universität Duisburg-Essen [Essen], Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), and Université de Lyon-École normale supérieure - Lyon (ENS Lyon)

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], High Energy Physics::Lattice, Object (grammar), Lattice theory, Distributive lattice, 0102 computer and information sciences, 01 natural sciences, Quantitative Biology::Cell Behavior, Combinatorics, Lattice (order), Mathematics::Category Theory, Subobject, 0101 mathematics, Mathematics, Adhesive categories, Algebra and Number Theory, Representation theorem, 010102 general mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Van Kampen colimits, 16. Peace & justice, Computational Mathematics, Informatik, Distributive property, 010201 computation theory & mathematics, Subobject classifier, Homomorphism
Abstract

International audience; It is a known fact that the subobjects of an object in an adhesive category form a distributive lattice. Building on this observation, in the paper we show how the representation theorem for finite distributive lattices applies to subobject lattices. In particular, we introduce a notion of irreducible object in an adhesive category, and we prove that any finite object of an adhesive category can be obtained as the colimit of its irreducible subobjects. Furthermore we show that every arrow between finite objects in an adhesive category can be interpreted as a lattice homomorphism between subobject lattices and, conversely, we characterize those homomorphisms between subobject lattices which can be seen as arrows.

Published
2011

15. Concurrency Can't Be Observed, Asynchronously

Author

Paolo Baldan, Fabio Gadducci, Filippo Bonchi, Giacoma Valentina Monreale, Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Dipartimento di Matematica Pura e Applicata [Padova], Università degli Studi di Padova = University of Padua (Unipd), Dipartimento di Informatica [Pisa], University of Pisa - Università di Pisa, Dipartimento di Informatica [Pisa] (DI), Concurrency, Mobility and Transactions (COMETE), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Universita degli Studi di Padova, ANR-10-LABX-0070,MILYON,Community of mathematics and fundamental computer science in Lyon(2010), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), and Bonchi, Filippo

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Theoretical computer science, Interleaving, Computer science, Process calculus, Concurrency, Visual specification, 0102 computer and information sciences, 02 engineering and technology, computer.software_genre, 01 natural sciences, Weak equivalence, Mathematics (miscellaneous), Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Barbed Semantics, contexts-as-labels paradigm, 0101 mathematics, Equivalence (formal languages), Non interleaving semantics, interactive systems, Programming language, 010102 general mathematics, barbed bisimilarity, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Petri net, 16. Peace & justice, Rotation formalisms in three dimensions, Computer Science Applications, Process Calculi, 010201 computation theory & mathematics, Asynchronous communication, asynchronous systems, 020201 artificial intelligence & image processing, Algorithm, computer
Abstract

The paper is devoted to an analysis of the concurrent features of asynchronous systems. A preliminary step is represented by the introduction of a non-interleaving extension of barbed equivalence. This notion is then exploited in order to prove thatconcurrency cannot be observedthrough asynchronous interactions, i.e., that the interleaving and concurrent versions of a suitable asynchronous weak equivalence actually coincide. The theory is validated on some case studies, related to nominal calculi (π-calculus) and visual specification formalisms (Petri nets). Additionally, we prove that a class of systems which is deemed (output-buffered) asynchronous, according to a characterization that was previously proposed in the literature, falls into our theory.

Published
2010

Catalog

Books, media, physical & digital resources
See catalog results