8 Search Results for "Laroussinie, François"

Document
DOI: 10.4230/LIPIcs.CONCUR.2024.4
Centralized vs Decentralized Monitors for Hyperproperties

Authors: Luca Aceto, Antonis Achilleos, Elli Anastasiadi, Adrian Francalanza, Daniele Gorla, and Jana Wagemaker

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
This paper focuses on the runtime verification of hyperproperties expressed in Hyper-recHML, an expressive yet simple logic for describing properties of sets of traces. To this end, we consider a simple language of monitors that observe sets of system executions and report verdicts w.r.t. a given Hyper-recHML formula. We first employ a unique omniscient monitor that centrally observes all system traces. Since centralised monitors are not ideal for distributed settings, we also provide a language for decentralized monitors, where each trace has a dedicated monitor; these monitors yield a unique verdict by communicating their observations to one another. For both the centralized and the decentralized settings, we provide a synthesis procedure that, given a formula, yields a monitor that is correct (i.e., sound and violation complete). A key step in proving the correctness of the synthesis for decentralized monitors is a result showing that, for each formula, the synthesized centralized monitor and its corresponding decentralized one are weakly bisimilar for a suitable notion of weak bisimulation.
Cite as

Luca Aceto, Antonis Achilleos, Elli Anastasiadi, Adrian Francalanza, Daniele Gorla, and Jana Wagemaker. Centralized vs Decentralized Monitors for Hyperproperties. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2024.4,
  author =	{Aceto, Luca and Achilleos, Antonis and Anastasiadi, Elli and Francalanza, Adrian and Gorla, Daniele and Wagemaker, Jana},
  title =	{{Centralized vs Decentralized Monitors for Hyperproperties}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{4:1--4:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.4},
  URN =		{urn:nbn:de:0030-drops-207763},
  doi =		{10.4230/LIPIcs.CONCUR.2024.4},
  annote =	{Keywords: Runtime Verification, hyperlogics, decentralization}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.14
As Soon as Possible but Rationally

Authors: Véronique Bruyère, Christophe Grandmont, and Jean-François Raskin

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
This paper addresses complexity problems in rational verification and synthesis for multi-player games played on weighted graphs, where the objective of each player is to minimize the cost of reaching a specific set of target vertices. In these games, one player, referred to as the system, declares his strategy upfront. The other players, composing the environment, then rationally make their moves according to their objectives. The rational behavior of these responding players is captured through two models: they opt for strategies that either represent a Nash equilibrium or lead to a play with a Pareto-optimal cost tuple.
Cite as

Véronique Bruyère, Christophe Grandmont, and Jean-François Raskin. As Soon as Possible but Rationally. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2024.14,
  author =	{Bruy\`{e}re, V\'{e}ronique and Grandmont, Christophe and Raskin, Jean-Fran\c{c}ois},
  title =	{{As Soon as Possible but Rationally}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{14:1--14:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.14},
  URN =		{urn:nbn:de:0030-drops-207869},
  doi =		{10.4230/LIPIcs.CONCUR.2024.14},
  annote =	{Keywords: Games played on graphs, rational verification, rational synthesis, Nash equilibrium, Pareto-optimality, quantitative reachability objectives}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.29
Strategic Dominance: A New Preorder for Nondeterministic Processes

Authors: Thomas A. Henzinger, Nicolas Mazzocchi, and N. Ege Saraç

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
We study the following refinement relation between nondeterministic state-transition models: model ℬ strategically dominates model 𝒜 iff every deterministic refinement of 𝒜 is language contained in some deterministic refinement of ℬ. While language containment is trace inclusion, and the (fair) simulation preorder coincides with tree inclusion, strategic dominance falls strictly between the two and can be characterized as "strategy inclusion" between 𝒜 and ℬ: every strategy that resolves the nondeterminism of 𝒜 is dominated by a strategy that resolves the nondeterminism of ℬ. Strategic dominance can be checked in 2-ExpTime by a decidable first-order Presburger logic with quantification over words and strategies, called resolver logic. We give several other applications of resolver logic, including checking the co-safety, co-liveness, and history-determinism of boolean and quantitative automata, and checking the inclusion between hyperproperties that are specified by nondeterministic boolean and quantitative automata.
Cite as

Thomas A. Henzinger, Nicolas Mazzocchi, and N. Ege Saraç. Strategic Dominance: A New Preorder for Nondeterministic Processes. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{henzinger_et_al:LIPIcs.CONCUR.2024.29,
  author =	{Henzinger, Thomas A. and Mazzocchi, Nicolas and Sara\c{c}, N. Ege},
  title =	{{Strategic Dominance: A New Preorder for Nondeterministic Processes}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{29:1--29:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.29},
  URN =		{urn:nbn:de:0030-drops-208011},
  doi =		{10.4230/LIPIcs.CONCUR.2024.29},
  annote =	{Keywords: quantitative automata, refinement relation, resolver, strategy, history-determinism}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.30
Around Classical and Intuitionistic Linear Processes

Authors: Juan C. Jaramillo, Dan Frumin, and Jorge A. Pérez

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
Curry-Howard correspondences between Linear Logic (LL) and session types provide a firm foundation for concurrent processes. As the correspondences hold for intuitionistic and classical versions of LL (ILL and CLL), we obtain two different families of type systems for concurrency. An open question remains: how do these two families exactly relate to each other? Based upon a translation from CLL to ILL due to Laurent, we provide two complementary answers, in the form of full abstraction results based on a typed observational equivalence due to Atkey. Our results elucidate hitherto missing formal links between seemingly related yet different type systems for concurrency.
Cite as

Juan C. Jaramillo, Dan Frumin, and Jorge A. Pérez. Around Classical and Intuitionistic Linear Processes. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{jaramillo_et_al:LIPIcs.CONCUR.2024.30,
  author =	{Jaramillo, Juan C. and Frumin, Dan and P\'{e}rez, Jorge A.},
  title =	{{Around Classical and Intuitionistic Linear Processes}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{30:1--30:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.30},
  URN =		{urn:nbn:de:0030-drops-208026},
  doi =		{10.4230/LIPIcs.CONCUR.2024.30},
  annote =	{Keywords: Process calculi, session types, linear logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2024.35
QLTL Model-Checking

Authors: François Laroussinie, Loriane Leclercq, and Arnaud Sangnier

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
Quantified LTL (QLTL) extends the temporal logic LTL with quantifications over atomic propositions. Several semantics exist to handle these quantifications, depending on the definition of executions over which formulas are interpreted: either infinite sequences of subsets of atomic propositions (aka the "tree semantics") or infinite sequences of control states combined with a labelling function that associates atomic propositions to the control states (aka the "structure semantics"). The main difference being that in the latter different occurrences of a control state should be labelled similarly. The tree semantics has been intensively studied from the complexity and expressivity point of view (especially in the work of Sistla [Sistla, 1983; Sistla et al., 1987]) for which the satisfiability and model-checking problems are known to be TOWER-complete. For the structure semantics, French has shown that the satisfiability problem is undecidable [French, 2003]. We study here the model-checking problem for QLTL under this semantics and prove that it is EXPSPACE-complete. We also show that the complexity drops down to PSPACE-complete for two specific cases of structures, namely path and flat ones.
Cite as

François Laroussinie, Loriane Leclercq, and Arnaud Sangnier. QLTL Model-Checking. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 35:1-35:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{laroussinie_et_al:LIPIcs.CSL.2024.35,
  author =	{Laroussinie, Fran\c{c}ois and Leclercq, Loriane and Sangnier, Arnaud},
  title =	{{QLTL Model-Checking}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{35:1--35:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.35},
  URN =		{urn:nbn:de:0030-drops-196783},
  doi =		{10.4230/LIPIcs.CSL.2024.35},
  annote =	{Keywords: Quantified Linear-time temporal logic, Model-cheking, Verification, Automata theory}
}
Document
DOI: 10.4230/LIPIcs.TIME.2019.11
From Quantified CTL to QBF

Authors: Akash Hossain and François Laroussinie

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

Abstract
QCTL extends the temporal logic CTL with quantifications over atomic propositions. This extension is known to be very expressive: QCTL allows us to express complex properties over Kripke structures (it is as expressive as MSO). Several semantics exist for the quantifications: here, we work with the structure semantics, where the extra propositions label the Kripke structure (and not its execution tree), and the model-checking problem is known to be PSPACE-complete in this framework. We propose a model-checking algorithm for QCTL based on a reduction to QBF. We consider several reduction strategies, and we compare them with a prototype (based on the SMT-solver Z3) on several examples.
Cite as

Akash Hossain and François Laroussinie. From Quantified CTL to QBF. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{hossain_et_al:LIPIcs.TIME.2019.11,
  author =	{Hossain, Akash and Laroussinie, Fran\c{c}ois},
  title =	{{From Quantified CTL to QBF}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{11:1--11:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.11},
  URN =		{urn:nbn:de:0030-drops-113699},
  doi =		{10.4230/LIPIcs.TIME.2019.11},
  annote =	{Keywords: Model-checking, Quantified CTL, QBF solvers, SAT based model-checking}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.28
On the Expressiveness of QCTL

Authors: Amélie David, Francois Laroussinie, and Nicolas Markey

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
QCTL extends the temporal logic CTL with quantification over atomic propositions. While the algorithmic questions for QCTL and its fragments with limited quantification depth are well-understood (e.g. satisfiability of QkCTL, with at most k nested blocks of quantifiers, is (k+1)-EXPTIME-complete), very few results are known about the expressiveness of this logic. We address such expressiveness questions in this paper. We first consider the distinguishing power of these logics (i.e., their ability to separate models), their relationship with behavioural equivalences, and their ability to capture the behaviours of finite Kripke structures with so-called characteristic formulas. We then consider their expressive power (i.e., their ability to express a property), showing that in terms of expressiveness the hierarchy QkCTL collapses at level 2 (in other terms, any QCTL formula can be expressed using at most two nested blocks of quantifiers).
Cite as

Amélie David, Francois Laroussinie, and Nicolas Markey. On the Expressiveness of QCTL. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 28:1-28:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{david_et_al:LIPIcs.CONCUR.2016.28,
  author =	{David, Am\'{e}lie and Laroussinie, Francois and Markey, Nicolas},
  title =	{{On the Expressiveness of QCTL}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{28:1--28:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.28},
  URN =		{urn:nbn:de:0030-drops-61643},
  doi =		{10.4230/LIPIcs.CONCUR.2016.28},
  annote =	{Keywords: Specification, Verification, Temporal Logic, Expressiveness, Tree automata}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.120
ATL with Strategy Contexts: Expressiveness and Model Checking

Authors: Arnaud Da Costa, François Laroussinie, and Nicolas Markey

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
We study the alternating-time temporal logics ATL and ATL* extended with strategy contexts: these make agents commit to their strategies during the evaluation of formulas, contrary to plain ATL and ATL* where strategy quantifiers reset previously selected strategies. We illustrate the important expressive power of strategy contexts by proving that they make the extended logics, namely ATLsc and ATLsc*, equally expressive: any formula in ATLsc* can be translated into an equivalent, linear-size ATLsc formula. Despite the high expressiveness of these logics, we~prove that their model-checking problems remain decidable by~designing a tree-automata-based algorithm for model-checking ATLsc* on the full class of $n$-player concurrent game structures.
Cite as

Arnaud Da Costa, François Laroussinie, and Nicolas Markey. ATL with Strategy Contexts: Expressiveness and Model Checking. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 120-132, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{dacosta_et_al:LIPIcs.FSTTCS.2010.120,
  author =	{Da Costa, Arnaud and Laroussinie, Fran\c{c}ois and Markey, Nicolas},
  title =	{{ATL with Strategy Contexts: Expressiveness and Model Checking}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{120--132},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.120},
  URN =		{urn:nbn:de:0030-drops-28589},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.120},
  annote =	{Keywords: alternating temporal logic, agent, strategy quantifier}
}
  • Refine by Author
  • 3 Laroussinie, François
  • 2 Markey, Nicolas
  • 1 Aceto, Luca
  • 1 Achilleos, Antonis
  • 1 Anastasiadi, Elli
  • Show More...

  • Refine by Classification
  • 5 Theory of computation → Logic and verification
  • 2 Theory of computation → Modal and temporal logics
  • 1 Software and its engineering → Formal methods
  • 1 Theory of computation → Formal languages and automata theory
  • 1 Theory of computation → Linear logic
  • Show More...

  • Refine by Keyword
  • 2 Verification
  • 1 Automata theory
  • 1 Expressiveness
  • 1 Games played on graphs
  • 1 Model-checking
  • Show More...

  • Refine by Type
  • 8 document

  • Refine by Publication Year
  • 5 2024
  • 1 2010
  • 1 2016
  • 1 2019

© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact