4 citations · 10 across the 10 of their papers we have counts for
11 papers
High-Level Message Sequence Charts: Satisfiability and Realizability Revisited
Benedikt Bollig, Marie Fortin, Paul Gastin
Message sequence charts (MSCs) visually represent interactions in distributed systems that communicate through FIFO channels. High-level MSCs (HMSCs) extend MSCs with choice, conca…
Reverse Engineering of Temporal Queries Mediated by LTL Ontologies
Marie Fortin, Boris Konev, Vladislav Ryzhikov +3
In reverse engineering of database queries, we aim to construct a query from a given set of answers and non-answers; it can then be used to explore the data further or as an explan…
HyperLTL Satisfiability Is Highly Undecidable, HyperCTL is Even Harder
Marie Fortin, Louwe B. Kuijer, Patrick Totzke +1
Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. The two most important such logics are H…
Unique Characterisability and Learnability of Temporal Instance Queries
Marie Fortin, Boris Konev, Vladislav Ryzhikov +3
We aim to determine which temporal instance queries can be uniquely characterised by a (polynomial-size) set of positive and negative temporal data examples. We start by considerin…
Interpolants and Explicit Definitions in Extensions of the Description Logic EL
Marie Fortin, Boris Konev, Frank Wolter
We show that the vast majority of extensions of the description logic do not enjoy the Craig interpolation nor the projective Beth definability property. This is the…
HyperLTL Satisfiability is -complete, HyperCTL* Satisfiability is -complete
Marie Fortin, Louwe B. Kuijer, Patrick Totzke +1
Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. The two most important such logics are H…
FO = FO3 for linear orders with monotone binary relations
Marie Fortin
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. Th…
It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with "Happened Before"
Benedikt Bollig, Marie Fortin, Paul Gastin
Message sequence charts (MSCs) naturally arise as executions of communicating finite-state machines (CFMs), in which finite-state processes exchange messages through unbounded FIFO…
Gossiping in Message-Passing Systems
Benedikt Bollig, Marie Fortin, Paul Gastin
We study the gossip problem in a message-passing environment: When a process receives a message, it has to decide whether the sender has more recent information on other processes…
Communicating Finite-State Machines and Two-Variable Logic
Benedikt Bollig, Marie Fortin, Paul Gastin
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 ar…
On parametrized verification of asynchronous, shared-memory pushdown systems
Marie Fortin, Anca Muscholl, Igor Walukiewicz
We consider the model of parametrized asynchronous shared-memory pushdown systems, as introduced in [Hague'11]. In a series of recent papers it has been shown that reachability in…