Daniela Petrisan

Daniela Petrisan

Assistant Professor, IRIF, Paris 7

News

• I am on maternity leave until 6 November 2018.
• I give a talk at the LSV seminar at l'ENS de Cachan on 30 April 2018.
• I will give an invited talk at CMCS 2018.
• Please consider submitting to CSL 2018.
• On 3 November 2017 I will give a talk about automata in glued vector spaces at the OASIS seminar in Oxford.
• I will attend the Shonan seminar on Enhanced Coinduction taking place in Japan, between 12-17 November 2017.
• Our paper Quantifiers on languages and codensity monads was accepted to LICS 2017. A long version is here.
• In November 2016 I will be a visiting scientist at Simons Institute for the Theory of Computing, University of California Berkeley.
• Please consider submiting to FSCD 2017.
• Please consider submiting to CALCO 2017.
• I am the PC chair of the CALCO Early Ideas 2017, affiliated with CALCO 2017.

Publications

Most recent (full list here)

• Up-To Techniques for Behavioural Metrics via Fibrations.
  Filippo Bonchi, Barbara König and Daniela Petrisan, CONCUR 2018
  [pdf] [abstract]

  Up-to techniques are a well-known method for enhancing coinductive proofs of behavioural equi- valences. We introduce up-to techniques for behavioural metrics between systems modelled as coalgebras and we provide abstract results to prove their soundness in a compositional way. In order to obtain a general framework, we need a systematic way to lift functors: we show that the Wasserstein lifting of a functor, introduced in a previous work, corresponds to a change of base in a fibrational sense. This observation enables us to reuse existing results about soundness of up-to techniques in a fibrational setting. We focus on the fibrations of predicates and relations valued in a quantale, for which pseudo-metric spaces are an example. To illustrate our approach we provide an example on distances between regular languages.

• Automata and minimization.
  Thomas Colcombet, Daniela Petrisan, SIGLOG News 4(2): 4-27 (2017)
  [link] [abstract]

  Already in the seventies, strong results illustrating the intimate relationship between category theory and automata theory have been described and are still investigated. In this column, we provide a uniform presentation of the basic concepts that underlie minimization results in automata theory. We then use this knowledge for introducing a new model of automata that is an hybrid of deterministic finite automata and automata weighted over a field. These automata are very natural, and enjoy minimization result by design. The presentation of this paper is indeed categorical in essence, but it assumes no prior knowledge from the reader. It is also non-conventional in that it is neither algebraic, nor co-algebraic oriented.

• A general account of coinduction up-to,
  F. Bonchi, D. Petrisan, D. Pous, J. Rot, Acta Informatica, (2016)
  [link] [abstract] [bibtex]

  @Article{BPPR2016,
     author={Bonchi, Filippo and Petri{\c{s}}an, Daniela and Pous, Damien and Rot, Jurriaan},
     title={A general account of coinduction up-to},
     journal=[Acta Informatica},
     year={2016},
     pages={1--64},
     issn={1432-0525},
     doi={10.1007/s00236-016-0271-4},
     url={http://dx.doi.org/10.1007/s00236-016-0271-4},
     }

  Bisimulation up-to enhances the coinductive proof method for bisimilarity, providing efficient proof techniques for checking properties of different kinds of systems. We prove the soundness of such techniques in a fibrational setting, building on the seminal work of Hermida and Jacobs. This allows us to systematically obtain up-to techniques not only for bisimilarity but for a large class of coinductive predicates modeled as coalgebras. The fact that bisimulations up to context can be safely used in any language specified by GSOS rules can also be seen as an instance of our framework, using the well-known observation by Turi and Plotkin that such languages form bialgebras. In the second part of the paper, we provide a new categorical treatment of weak bisimilarity on labeled transition systems and we prove the soundness of up-to context for weak bisimulations of systems specified by cool rule formats, as defined by Bloom to ensure congruence of weak bisimilarity. The weak transition systems obtained from such cool rules give rise to lax bialgebras, rather than to bialgebras. Hence, to reach our goal, we extend the categorical framework developed in the first part to an ordered setting.

• Automata in the Category of Glued Vector Spaces
  Thomas Colcombet, Daniela Petrisan, MFCS 2017
  [link] [abstract]

  In this paper we adopt a category-theoretic approach to the conception of automata classes enjoying minimization by design. The main instantiation of our construction is a new class of automata that are hybrid between deterministic automata and automata weighted over a field.

• Automata minimization: a functorial approach
  Thomas Colcombet, Daniela Petrisan, CALCO 2017
  [link] [abstract]

  In this paper we regard languages and their acceptors - such as deterministic or weighted automata, transducers, or monoids - as functors from input categories that specify the type of the languages and of the machines to categories that specify the type of outputs. Our results are as follows: a) We provide sufficient conditions on the output category so that minimization of the corresponding automata is guaranteed. b) We show how to lift adjunctions between the categories for output values to adjunctions between categories of automata. c) We show how this framework can be applied to several phenomena in automata theory, starting with determinization and minimization (previously studied from a coalgebraic and duality theoretic perspective). We apply in particular these techniques to Choffrut’s minimization algorithm for subsequential transducers and revisit Brzozowski’s minimization algorithm.

• Quantifiers on languages and codensity monads,
  Mai Gehrke, Daniela Petrisan, Luca Reggio, LICS 2017
  [link] [abstract] [arxiv long version] [conference version]

  This paper contributes to the techniques of topoalgebraic recognition for languages beyond the regular setting as they relate to logic on words. In particular, we provide a general construction on recognisers corresponding to adding one layer of various kinds of quantifiers and prove a related Reutenauer-type theorem. Our main tools are codensity monads and duality theory. Our construction yields, in particular, a new characterisation of the profinite monad of the free S-semimodule monad for finite and commutative semirings S, which generalises our earlier insight that the Vietoris monad on Boolean spaces is the codensity monad of the finite powerset functor.

• The Schutzenberger Product for Syntactic Spaces. ,
  M. Gehrke, D. Petrisan, L. Reggio, ICALP 2016
  [link] [abstract]

  Starting from Boolean algebras of languages closed under quotients and using duality theoretic insights, we derive the notion of Boolean spaces with internal monoids as recognisers for arbitrary formal languages of finite words over finite alphabets. This leads to recognisers and syntactic spaces in a setting that is well-suited for applying tools from Stone duality as applied in semantics. The main focus of the paper is the development of topo-algebraic constructions pertinent to the treatment of languages given by logic formulas. In particular, using the standard semantic view of quantification as projection, we derive a notion of Schützenberger product for Boolean spaces with internal monoids. This makes heavy use of the Vietoris construction - and its dual functor - which is central to the coalgebraic treatment of classical modal logic. We show that the unary Schützenberger product for spaces yields a recogniser for the language of all models of the formula EXISTS x.phi(x), when applied to a recogniser for the language of all models of phi(x). Further, we generalise global and local versions of the theorems of Schützenberger and Reutenauer characterising the languages recognised by the binary Schützenberger product. Finally, we provide an equational characterisation of Boolean algebras obtained by local Schützenberger product with the one element space based on an Egli-Milner type condition on generalised factorisations of ultrafilters on words.

• Lax Bialgebras and Up-To Techniques for Weak Bisimulations,
  F. Bonchi, D. Petrisan, D. Pous, J. Rot, CONCUR 2015
  [abstract]

  Up-to techniques are useful tools for optimising proofs of behavioural equivalence of processes. Bisimulations up-to context can be safely used in any language specified by GSOS rules. We showed this result in a previous paper by exploiting the well-known observation by Turi and Plotkin that such languages form bialgebras. In this paper, we prove the soundness of up-to contextual closure for weak bisimilations of systems specified by cool rule formats, as defined by Bloom to ensure congruence of weak bisimilarity. However, the weak transition systems obtained from such cool rules give rise to lax bialgebras, rather than to bialgebras. Hence, to reach our goal, we extend our previously developed categorical framework to an ordered enriched setting.

• Nominal techniques for variables with interleaving scopes,
  D. Ghica, M.J. Gabbay, D. Petrisan. CSL 2015
• Nominal Kleene Coalgebra,
  D. Kozen, K. Mamouras, D. Petrisan, A. Silva, ICALP 2015
  [abstract] [long version]

  We develop the coalgebraic theory of nominal Kleene algebra, including an alternative language-theoretic semantics, a nominal extension of the Brzozowski derivative, and a bisimulation-based decision procedure for the equational theory.

• Approximation of Nested Fixpoints -- A Coalgebraic View of Parametric Dataypes,
  A. Kurz, A. Pardo, D. Petrisan, P. Severi and F-J. de Vries, CALCO 2015
  [abstract]

  The question addressed in this paper is how to correctly approximate infinite data given by systems of simultaneous corecursive definitions. We devise a categorical framework for reasoning about regular datatypes, that is, datatypes closed under products, coproducts and fixpoints. We argue that the right methodology is on one hand coalgebraic (to deal with possible non-termination and infinite data) and on the other hand 2-categorical (to deal with parameters in a disciplined manner). We prove a coalgebraic version of Beki{\v c} lemma that allows us to reduce simultaneous fixpoints to a single fix point. Thus a possibly infinite object of interest is regarded as a final coalgebra of a many-sorted polynomial functor and can be seen as a limit of finite approximants. As an application, we prove correctness of a generic function that calculates the approximants on a large class of data types.

• Coinduction up-to in a fibrational setting,
  F. Bonchi, D. Petrisan, D. Pous, J. Rot, CSL-LICS 2014
  [link] [arxiv link] [conference version] [abstract] [bibtex]

  @inproceedings{DBLP:conf/csl/BonchiPPR14,,
     author = {Filippo Bonchi and Daniela Petrisan and Damien Pous and Jurriaan Rot},
     title = {Coinduction up-to in a fibrational setting},
     booktitle = {Joint Meeting of the Twenty-Third {EACSL} Annual Conference on Computer Science Logic {(CSL)} and the Twenty-Ninth Annual {ACM/IEEE} Symposium on Logic in Computer Science (LICS), {CSL-LICS} '14, Vienna, Austria, July 14 - 18, 2014},
     pages = {20},
     year = {2014},
     url = {http://doi.acm.org/10.1145/2603088.2603149},
     doi = {10.1145/2603088.2603149},
     }

  Bisimulation up-to enhances the coinductive proof method for bisimilarity, providing efficient proof techniques for checking properties of different kinds of systems. We prove the soundness of such techniques in a fibrational setting, building on the seminal work of Hermida and Jacobs. This allows us to systematically obtain up-to techniques not only for bisimilarity but for a large class of coinductive predicates modelled as coalgebras. By tuning the parameters of our framework, we obtain novel techniques for unary predicates and nominal automata, a variant of the GSOS rule format for similarity, and a new categorical treatment of weak bisimilarity.

Teaching

• 2017-18: This fall I am teaching a TD in Algorithms for L3 students at Paris 7. The course's webpage is here.
• 2012-13: As a lecturer/research associate at the University of Leicester, I was responsible for two courses:
  • Data Structures and Development Environments (approx. 100 students, L1 level)
  • Operating Systems, Networks and Distributed Systems (approx. 70 students, L2 level)
• 2010-2011 I supervised seven MSc projects at the University of Leicester
• 2011-2012 I supervised eight MSc projects at the University of Leicester
• 2007–2011: I have been teaching assistant for several modules at the University of Leicester:
  Java for Bioinformatics (MSc module), Program Design, Databases and Web Applications, Software Reliability (MSc module), Functional Programming, Logic Programming, Logic and Problem Solving, Discrete Structures, Information Management

Activities

• I am in the Publicity committee of ACM SIGLOG.
• I have served on several Program Committes: CSL 2018, MFPS 2017, FSCD 2017, CALCO 2017, CONCUR 2016, CMCS 2016, CALCO 2015, MFPS 30 , CMCS 2014, CALCO 2013, ICE 2013, CMCS 2012
• I was the Program Chair of CALCO 2017 Early Ideas affiliated Workshop
• Invited talks: CMCS 2018, ALCOP 2017, CALCO 2015, MFPS 2015 (invited tutorial speaker)

Contact

Email: petrisanirif.fr
Office: 4016, Bâtiment Sophie Germain, 8 place Aurélie Nemours, 75013 Paris
Work phone: +33 (0)1 57 27 94 00
Postal address: IRIF, Université Paris Diderot - Paris 7 - Case 7014, F-75205 Paris Cedex 13