Daniela Petrisan
Postdoctoral researcher, CNRS, IRIF, Paris 7
-
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.
Most recent (full list here)
- 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.
-
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
-
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)
Email: petrisanirif.fr
Office: 4029a, Bâtiment Sophie Germain, 8 place Aurélie Nemours, 75013 Paris
Work phone: +33 (0)1 57 27 92 21
Postal address: IRIF, Université Paris Diderot - Paris 7 - Case 7014, F-75205 Paris Cedex 13
I am a researcher working on Mai Gehrke's ERC
project DuaLL
in the Automata team
of IRIF
at Université
Paris Diderot - Paris 7. Before joining IRIF, I worked
in the Intelligent Systems group at Radboud University
Nijmegen and I was a researcher on the ANR
project PiCoq
in the
Plume team
of École Normale Supérieure
Lyon. Previously I had various positions including a fixed-term
lectureship and a research associate position at
the University of Leicester.