4 Search Results for "Bérard, Béatrice"


Document
Timed Basic Parallel Processes

Authors: Lorenzo Clemente, Piotr Hofman, and Patrick Totzke

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
Timed basic parallel processes (TBPP) extend communication-free Petri nets (aka. BPP or commutative context-free grammars) by a global notion of time. TBPP can be seen as an extension of timed automata (TA) with context-free branching rules, and as such may be used to model networks of independent timed automata with process creation. We show that the coverability and reachability problems (with unary encoded target multiplicities) are PSPACE-complete and EXPTIME-complete, respectively. For the special case of 1-clock TBPP, both are NP-complete and hence not more complex than for untimed BPP. This contrasts with known super-Ackermannian-completeness and undecidability results for general timed Petri nets. As a result of independent interest, and basis for our NP upper bounds, we show that the reachability relation of 1-clock TA can be expressed by a formula of polynomial size in the existential fragment of linear arithmetic, which improves on recent results from the literature.

Cite as

Lorenzo Clemente, Piotr Hofman, and Patrick Totzke. Timed Basic Parallel Processes. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{clemente_et_al:LIPIcs.CONCUR.2019.15,
  author =	{Clemente, Lorenzo and Hofman, Piotr and Totzke, Patrick},
  title =	{{Timed Basic Parallel Processes}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{15:1--15:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.15},
  URN =		{urn:nbn:de:0030-drops-109171},
  doi =		{10.4230/LIPIcs.CONCUR.2019.15},
  annote =	{Keywords: Timed Automata, Petri Nets}
}
Document
Hyper Partial Order Logic

Authors: Béatrice Bérard, Stefan Haar, and Loic Hélouët

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)


Abstract
We define HyPOL, a local hyper logic for partial order models, expressing properties of sets of runs. These properties depict shapes of causal dependencies in sets of partially ordered executions, with similarity relations defined as isomorphisms of past observations. Unsurprisingly, since comparison of projections are included, satisfiability of this logic is undecidable. We then address model checking of HyPOL and show that, already for safe Petri nets, the problem is undecidable. Fortunately, sensible restrictions of observations and nets allow us to bring back model checking of HyPOL to a decidable problem, namely model checking of MSO on graphs of bounded treewidth.

Cite as

Béatrice Bérard, Stefan Haar, and Loic Hélouët. Hyper Partial Order Logic. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 20:1-20:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{berard_et_al:LIPIcs.FSTTCS.2018.20,
  author =	{B\'{e}rard, B\'{e}atrice and Haar, Stefan and H\'{e}lou\"{e}t, Loic},
  title =	{{Hyper Partial Order Logic}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{20:1--20:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.20},
  URN =		{urn:nbn:de:0030-drops-99190},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.20},
  annote =	{Keywords: Partial orders, logic, hyper-logic}
}
Document
Finite Bisimulations for Dynamical Systems with Overlapping Trajectories

Authors: Béatrice Bérard, Patricia Bouyer, and Vincent Jugé

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)


Abstract
Having a finite bisimulation is a good feature for a dynamical system, since it can lead to the decidability of the verification of reachability properties. We investigate a new class of o-minimal dynamical systems with very general flows, where the classical restrictions on trajectory intersections are partly lifted. We identify conditions, that we call Finite and Uniform Crossing: When Finite Crossing holds, the time-abstract bisimulation is computable and, under the stronger Uniform Crossing assumption, this bisimulation is finite and definable.

Cite as

Béatrice Bérard, Patricia Bouyer, and Vincent Jugé. Finite Bisimulations for Dynamical Systems with Overlapping Trajectories. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 26:1-26:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{berard_et_al:LIPIcs.CSL.2018.26,
  author =	{B\'{e}rard, B\'{e}atrice and Bouyer, Patricia and Jug\'{e}, Vincent},
  title =	{{Finite Bisimulations for Dynamical Systems with Overlapping Trajectories}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{26:1--26:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.26},
  URN =		{urn:nbn:de:0030-drops-96932},
  doi =		{10.4230/LIPIcs.CSL.2018.26},
  annote =	{Keywords: Reachability properties, dynamical systems, o-minimal structures, intersecting trajectories, finite bisimulations}
}
Document
Probabilistic Disclosure: Maximisation vs. Minimisation

Authors: Béatrice Bérard, Serge Haddad, and Engel Lefaucheux

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)


Abstract
We consider opacity questions where an observation function provides to an external attacker a view of the states along executions and secret executions are those visiting some state from a fixed subset. Disclosure occurs when the observer can deduce from a finite observation that the execution is secret, the epsilon-disclosure variant corresponding to the execution being secret with probability greater than 1 - epsilon. In a probabilistic and non deterministic setting, where an internal agent can choose between actions, there are two points of view, depending on the status of this agent: the successive choices can either help the attacker trying to disclose the secret, if the system has been corrupted, or they can prevent disclosure as much as possible if these choices are part of the system design. In the former situation, corresponding to a worst case, the disclosure value is the supremum over the strategies of the probability to disclose the secret (maximisation), whereas in the latter case, the disclosure is the infimum (minimisation). We address quantitative problems (comparing the optimal value with a threshold) and qualitative ones (when the threshold is zero or one) related to both forms of disclosure for a fixed or finite horizon. For all problems, we characterise their decidability status and their complexity. We discover a surprising asymmetry: on the one hand optimal strategies may be chosen among deterministic ones in maximisation problems, while it is not the case for minimisation. On the other hand, for the questions addressed here, more minimisation problems than maximisation ones are decidable.

Cite as

Béatrice Bérard, Serge Haddad, and Engel Lefaucheux. Probabilistic Disclosure: Maximisation vs. Minimisation. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 13:1-13:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{berard_et_al:LIPIcs.FSTTCS.2017.13,
  author =	{B\'{e}rard, B\'{e}atrice and Haddad, Serge and Lefaucheux, Engel},
  title =	{{Probabilistic Disclosure: Maximisation vs. Minimisation}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{13:1--13:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.13},
  URN =		{urn:nbn:de:0030-drops-83844},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.13},
  annote =	{Keywords: Partially observed systems, Opacity, Markov chain, Markov decision process}
}
  • Refine by Author
  • 3 Bérard, Béatrice
  • 1 Bouyer, Patricia
  • 1 Clemente, Lorenzo
  • 1 Haar, Stefan
  • 1 Haddad, Serge
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Logic and verification
  • 1 Theory of computation → Timed and hybrid models

  • Refine by Keyword
  • 1 Markov chain
  • 1 Markov decision process
  • 1 Opacity
  • 1 Partial orders
  • 1 Partially observed systems
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 3 2018
  • 1 2019

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail