@comment{{B-arxiv16,
author = Bollig, Benedikt,
affiliation = aff-LSVmexico,
title = One-Counter Automata with Counter Visibility,
institution = Computing Research Repository,
number = 1602.05940,
month = feb,
nmonth = 2,
year = 2016,
type = RR,
axeLSV = mexico,
NOcontrat = "",
url = http://arxiv.org/abs/1602.05940,
PDF = "http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
lsvdate-new = 20160222,
lsvdate-upd = 20160222,
lsvdate-pub = 20160222,
lsv-category = "rapl",
wwwpublic = "public and ccsb",
note = 18~pages,
abstract = "In a one-counter automaton (OCA), one can read a letter
from some finite alphabet, increment and decrement the counter by
one, or test it for zero. It is well-known that universality and
language inclusion for OCAs are undecidable. We consider here OCAs
with counter visibility: Whenever the automaton produces a letter,
it outputs the current counter value along with~it. Hence, its
language is now a set of words over an infinite alphabet. We show
that universality and inclusion for that model are in PSPACE, thus
no harder than the corresponding problems for finite automata, which
can actually be considered as a special case. In fact, we show that
OCAs with counter visibility are effectively determinizable and
closed under all boolean operations. As~a~strict generalization, we
subsequently extend our model by registers. The general nonemptiness
problem being undecidable, we impose a bound on the number of
register comparisons and show that the corresponding nonemptiness
problem is NP-complete.",
}}
@inproceedings{FG-fossacs16,
address = {Eindhoven, The~Netherlands},
month = apr,
year = 2016,
volume = {9634},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Jacobs, Bart and L{\"o}ding, Christof},
acronym = {{FoSSaCS}'16},
booktitle = {{P}roceedings of the 19th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'16)},
author = {Fortin, Marie and Gastin, Paul},
title = {Verification of parameterized communicating automata via split-width},
pages = {197-213},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FG-fossacs16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FG-fossacs16.pdf},
doi = {10.1007/978-3-662-49630-5_12},
abstract = {We~study verification problems for distributed systems
communicating via unbounded FIFO channels. The number of processes
of the system as well as the communication topology are not fixed
a~priori. Systems are given by parameterized communicating automata
(PCAs) which can be run on any communication topology of bounded
degree, with arbitrarily many processes. Such systems are Turing
powerful so we concentrate on under-approximate verification. We
extend the notion of split-width to behaviors of PCAs. We show that
emptiness, reachability and model-checking problems of PCAs are
decidable when restricted to behaviors of bounded split-width.
Reachability and emptiness are EXPTIME-complete, but only polynomial
in the size of the PCA. We also describe several concrete classes of
bounded split-width, for which we prove similar results.}
}
@inproceedings{BFG-stacs18,
address = {Caen, France},
month = feb,
volume = {96},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Niedermeier, Rolf and Vall{\'e}e, Brigitte},
acronym = {{STACS}'18},
booktitle = {{P}roceedings of the 35th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'18)},
author = {Bollig, Benedikt and Fortin, Marie and Gastin, Paul},
title = {Communicating Finite-State Machines and Two-Variable Logic},
pages = {17:1-17:14},
year = {2018},
doi = {10.4230/LIPIcs.STACS.2018.17},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/8529/pdf/LIPIcs-STACS-2018-17.pdf},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=8529},
abstract = {Communicating finite-state machines are a fundamental, well-studied model of finite-state processes that communicate via unbounded first-in first-out channels. We show that they are expressively equivalent to existential MSO logic with two first-order variables and the order relation.}
}
@inproceedings{FMW-cav17,
address = {Heidelberg, Germany},
month = jul,
volume = {10427},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kuncak, Viktor and Majumdar, Rupak},
acronym = {{CAV}'17},
booktitle = {{P}roceedings of the 29th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'17)},
author = {Fortin, Marie and Muscholl, Anca and Walukiewicz, Igor},
title = {Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems},
pages = {155-175},
year = {2017},
doi = {10.1007/978-3-319-63390-9_9},
url = {https://arxiv.org/abs/1606.08707},
abstract = {}
}
@inproceedings{BFG-concur18,
address = {Beijing, China},
month = sep,
year = 2018,
volume = {118},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Schewe, Sven and Zhang, Lijun},
acronym = {{CONCUR}'18},
booktitle = {{P}roceedings of the 29th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'18)},
author = {Bollig, Benedikt and Fortin, Marie and Gastin, Paul},
title = {It Is Easy to Be Wise After the Event: Communicating Finite-State
Machines Capture First-Order Logic with ''Happened Before''},
pages = {7:1-7:17},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9545},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9545/pdf/LIPIcs-CONCUR-2018-7.pdf},
doi = {10.4230/LIPIcs.CONCUR.2018.7},
abstract = {Message sequence charts (MSCs) naturally arise as executions of communicating finite-state machines (CFMs), in which finite-state processes exchange messages through unbounded FIFO channels. We study the first-order logic of MSCs, featuring Lamport's happened-before relation. We introduce a star-free version of propositional dynamic logic (PDL) with loop and converse. Our main results state that (i) every first-order sentence can be transformed into an equivalent star-free PDL sentence (and conversely), and (ii) every star-free PDL sentence can be translated into an equivalent CFM. This answers an open question and settles the exact relation between CFMs and fragments of monadic second-order logic. As a byproduct, we show that first-order logic over MSCs has the three-variable property.}
}
@mastersthesis{m2-Fortin,
author = {Fortin, Marie},
title = {{Verification of distributed systems with parameterized network topology}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2015},
month = sep
}
@inproceedings{Fortin-icalp19,
address = {Patras, Greece},
month = jul,
volume = {132},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chatzigiannakis, Ioannis and Merelli, Emanuela},
acronym = {{ICALP}'19},
booktitle = {{P}roceedings of the 46th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'19)},
author = {Fortin, Marie},
title = {FO = FO3 for linear orders with monotone binary relations},
year = 2019,
pages = {116:1-116:13},
doi = {10.4230/LIPIcs.ICALP.2019.116},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10692/pdf/LIPIcs-ICALP-2019-116.pdf},
url = {http://drops.dagstuhl.de/opus/volltexte/2019/10692/},
abstract = {We show that over the class of linear orders with additional
binary relations satisfying some monotonicity conditions, monadic first-order
logic has the three-variable property. This generalizes (and gives a new proof
of) several known results, including the fact that monadic first-order logic
has the three-variable property over linear orders, as well as over
(R, <, +1), and answers some open questions mentioned in a paper from
Antonopoulos, Hunter, Raza and Worrell [FoSSaCS 2015]. Our proof is based on
a translation of monadic first-order logic formulas into formulas of a star-free
variant of Propositional Dynamic Logic, which are in turn easily expressible in
monadic first-order logic with three variables.}
}
@phdthesis{fortin-phd2020,
author = {Fortin, Marie},
title = {{Expressivity of first-order logic, star-free propositional dynamic logic and communicating automata}},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2020,
month = nov,
url = {https://tel.archives-ouvertes.fr/tel-03079438},
pdf = {https://tel.archives-ouvertes.fr/tel-03079438/document}
}
@article{BFG-jcss20,
publisher = {Elsevier Science Publishers},
journal = {Journal of Computer and System Sciences},
author = {Benedikt Bollig and Marie Fortin and Paul Gastin},
title = {Communicating Finite-State Machines, First-Order Logic, and Star-Free Propositional Dynamic Logic},
pages = {22-53},
doi = {10.1016/j.jcss.2020.06.006},
year = {2020},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFG20-JCSS.pdf},
abstract = {Message sequence charts (MSCs) naturally arise as executions of communicating
finite-state machines (CFMs), in which finite-state processes exchange
messages through unbounded FIFO channels. We study the first-order logic of
MSCs, featuring Lamport's happened-before relation. To this end, we introduce a star-free
version of propositional dynamic logic (PDL) with loop and converse. Our main
results state that (i) every first-order sentence can be transformed into an
equivalent star-free PDL sentence (and conversely), and (ii) every star-free
PDL sentence can be translated into an equivalent CFM. This answers an open
question and settles the exact relation between CFMs and fragments of monadic
second-order logic. As a byproduct, we show that first-order logic over MSCs
has the three-variable property.}
}
This file was generated by bibtex2html 1.98.