Search Results

Documents authored by Legay, Axel

Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.394
An omega-Algebra for Real-Time Energy Problems

Authors: David Cachera, Uli Fahrenberg, and Axel Legay

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
We develop a *-continuous Kleene omega-algebra of real-time energy functions. Together with corresponding automata, these can be used to model systems which can consume and regain energy (or other types of resources) depending on available time. Using recent results on *-continuous Kleene omega-algebras and computability of certain manipulations on real-time energy functions, it follows that reachability and Büchi acceptance in real-time energy automata can be decided in a static way which only involves manipulations of real-time energy functions.
Cite as

David Cachera, Uli Fahrenberg, and Axel Legay. An omega-Algebra for Real-Time Energy Problems. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 394-407, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{cachera_et_al:LIPIcs.FSTTCS.2015.394,
  author =	{Cachera, David and Fahrenberg, Uli and Legay, Axel},
  title =	{{An omega-Algebra for Real-Time Energy Problems}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{394--407},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.394},
  URN =		{urn:nbn:de:0030-drops-56511},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.394},
  annote =	{Keywords: Energy problem, Real time, Star-continuous Kleene algebra}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2015.101
Partial Higher-dimensional Automata

Authors: Uli Fahrenberg and Axel Legay

Published in: LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

Abstract
We propose a generalization of higher-dimensional automata, partial HDA. Unlike HDA, and also extending event structures and Petri nets, partial HDA can model phenomena such as priorities or the disabling of an event by another event. Using open maps and unfoldings, we introduce a natural notion of (higher-dimensional) bisimilarity for partial HDA and relate it to history-preserving bisimilarity and split bisimilarity. Higher-dimensional bisimilarity has a game characterization and is decidable in polynomial time.
Cite as

Uli Fahrenberg and Axel Legay. Partial Higher-dimensional Automata. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 101-115, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{fahrenberg_et_al:LIPIcs.CALCO.2015.101,
  author =	{Fahrenberg, Uli and Legay, Axel},
  title =	{{Partial Higher-dimensional Automata}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{101--115},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Moss, Lawrence S. and Sobocinski, Pawel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.101},
  URN =		{urn:nbn:de:0030-drops-55295},
  doi =		{10.4230/LIPIcs.CALCO.2015.101},
  annote =	{Keywords: higher-dimensional automata, bisimulation}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.517
Information Leakage of Non-Terminating Processes

Authors: Fabrizio Biondi, Axel Legay, Bo Friis Nielsen, Pasquale Malacaria, and Andrzej Wasowski

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
In recent years, quantitative security techniques have been providing effective measures of the security of a system against an attacker. Such techniques usually assume that the system produces a finite amount of observations based on a finite amount of secret bits and terminates, and the attack is based on these observations. By modeling systems with Markov chains, we are able to measure the effectiveness of attacks on non-terminating systems. Such systems do not necessarily produce a finite amount of output and are not necessarily based on a finite amount of secret bits. We provide characterizations and algorithms to define meaningful measures of security for non-terminating systems, and to compute them when possible. We also study the bounded versions of the problems, and show examples of non-terminating programs and how their effectiveness in protecting their secret can be measured.
Cite as

Fabrizio Biondi, Axel Legay, Bo Friis Nielsen, Pasquale Malacaria, and Andrzej Wasowski. Information Leakage of Non-Terminating Processes. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 517-529, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{biondi_et_al:LIPIcs.FSTTCS.2014.517,
  author =	{Biondi, Fabrizio and Legay, Axel and Nielsen, Bo Friis and Malacaria, Pasquale and Wasowski, Andrzej},
  title =	{{Information Leakage of Non-Terminating Processes}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{517--529},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.517},
  URN =		{urn:nbn:de:0030-drops-48683},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.517},
  annote =	{Keywords: Quantitative information flow, Markov chain, information leakage, infinite execution}
}
Document
DOI: 10.4230/DagRep.4.1.104
Quantitative Models: Expressiveness, Analysis, and New Applications (Dagstuhl Seminar 14041)

Authors: Manfred Droste, Paul Gastin, Kim Gulstrand Larsen, and Axel Legay

Published in: Dagstuhl Reports, Volume 4, Issue 1 (2014)

Abstract
From Jan. 19 to Jan. 24, 2014, "Quantitative Models: Expressiveness, Analysis, and New Applications" was held in Schloss Dagstuhl-Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Manfred Droste, Paul Gastin, Kim Gulstrand Larsen, and Axel Legay. Quantitative Models: Expressiveness, Analysis, and New Applications (Dagstuhl Seminar 14041). In Dagstuhl Reports, Volume 4, Issue 1, pp. 104-124, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{droste_et_al:DagRep.4.1.104,
  author =	{Droste, Manfred and Gastin, Paul and Larsen, Kim Gulstrand and Legay, Axel},
  title =	{{Quantitative Models: Expressiveness, Analysis, and New Applications (Dagstuhl Seminar 14041)}},
  pages =	{104--124},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{4},
  number =	{1},
  editor =	{Droste, Manfred and Gastin, Paul and Larsen, Kim Gulstrand and Legay, Axel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.4.1.104},
  URN =		{urn:nbn:de:0030-drops-45374},
  doi =		{10.4230/DagRep.4.1.104},
  annote =	{Keywords: quantitative models, quantitative analysis, timed and hybrid systems, probabilistic systems, weighted automata, systems biology, smart grid}
}
Document
DOI: 10.4230/DagRep.3.2.144
Analysis, Test and Verification in The Presence of Variability (Dagstuhl Seminar 13091)

Authors: Paulo Borba, Myra B. Cohen, Axel Legay, and Andrzej Wasowski

Published in: Dagstuhl Reports, Volume 3, Issue 2 (2013)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 13091 "Analysis, Test and Verification in The Presence of Variability". The seminar had the goal of consolidating and stimulating research on analysis of software models with variability, enabling the design of variability-aware tool chains. We brought together 46 key researchers from three continents, working on quality assurance challenges that arise from introducing variability, and some who do not work with variability, but that are experts in their respective areas in the broader domain of software analysis or testing research. As a result of interactions triggered by sessions of different formats, the participants were able to classify their approaches with respect to a number of dimensions that helped to identify similarities and differences that have already been useful to improve understanding and foster new collaborations among the participants.
Cite as

Paulo Borba, Myra B. Cohen, Axel Legay, and Andrzej Wasowski. Analysis, Test and Verification in The Presence of Variability (Dagstuhl Seminar 13091). In Dagstuhl Reports, Volume 3, Issue 2, pp. 144-170, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{borba_et_al:DagRep.3.2.144,
  author =	{Borba, Paulo and Cohen, Myra B. and Legay, Axel and Wasowski, Andrzej},
  title =	{{Analysis, Test and Verification in The Presence of Variability (Dagstuhl Seminar 13091)}},
  pages =	{144--170},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{3},
  number =	{2},
  editor =	{Borba, Paulo and Cohen, Myra B. and Legay, Axel and Wasowski, Andrzej},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.3.2.144},
  URN =		{urn:nbn:de:0030-drops-40207},
  doi =		{10.4230/DagRep.3.2.144},
  annote =	{Keywords: Verification, Program Analysis, Testing, Semantics of Programming Languages, Software Engineering}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2011.103
The Quantitative Linear-Time--Branching-Time Spectrum

Authors: Uli Fahrenberg, Axel Legay, and Claus Thrane

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

Abstract
We present a distance-agnostic approach to quantitative verification. Taking as input an unspecified distance on system traces, or executions, we develop a game-based framework which allows us to define a spectrum of different interesting system distances corresponding to the given trace distance. Thus we extend the classic linear-time--branching-time spectrum to a quantitative setting, parametrized by trace distance. We also provide fixed-point characterizations of all system distances, and we prove a general transfer principle which allows us to transfer counterexamples from the qualitative to the quantitative setting,showing that all system distances are mutually topologically inequivalent.
Cite as

Uli Fahrenberg, Axel Legay, and Claus Thrane. The Quantitative Linear-Time--Branching-Time Spectrum. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 103-114, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{fahrenberg_et_al:LIPIcs.FSTTCS.2011.103,
  author =	{Fahrenberg, Uli and Legay, Axel and Thrane, Claus},
  title =	{{The Quantitative Linear-Time--Branching-Time Spectrum}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{103--114},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.103},
  URN =		{urn:nbn:de:0030-drops-33324},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.103},
  annote =	{Keywords: Quantitative verification, System distance, Distance hierarchy, Linear time, Branching time}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2009.2309
On Timed Alternating Simulation for Concurrent Timed Games

Authors: Laura Bozzelli, Axel Legay, and Sophie Pinchinat

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

Abstract
We address the problem of alternating simulation refinement for concurrent timed games (\TG). We show that checking timed alternating simulation between\TG is \EXPTIME-complete, and provide a logical characterization of thispreorder in terms of a meaningful fragment of a new logic, \TAMTLSTAR.\TAMTLSTAR is an action-based timed extension of standard alternating-timetemporal logic \ATLSTAR, which allows to quantify on strategies where thedesignated player is not responsible for blocking time. While for full \TAMTLSTAR, model-checking \TG is undecidable, we show that for its fragment \TAMTL, corresponding to the timed version of \ATL, in \EXPTIME.
Cite as

Laura Bozzelli, Axel Legay, and Sophie Pinchinat. On Timed Alternating Simulation for Concurrent Timed Games. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 85-96, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{bozzelli_et_al:LIPIcs.FSTTCS.2009.2309,
  author =	{Bozzelli, Laura and Legay, Axel and Pinchinat, Sophie},
  title =	{{On Timed Alternating Simulation for Concurrent Timed Games}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{85--96},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2309},
  URN =		{urn:nbn:de:0030-drops-23092},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2309},
  annote =	{Keywords: Concurrent Timed Games, Timed Alternating Simulation, Timed Alternating Temporal Logics}
}
Document
DOI: 10.4230/OASIcs.TrustworthySW.2006.766
An Introduction to the Tool Ticc

Authors: Axel Legay, Luca de Alfaro, and Marco Faella

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)

Abstract
This paper is a tutorial introduction to the sociable interface model of [12] and its underlying tool \textsc{Tcc}. The paper starts with a survey of the theory of interfaces and then introduces the sociable interface model that is a game-based model with rich communication primitives to facilitate the modeling of software and distributed systems. The model and its main features are then intensivelly discussed and illustrated using the tool \textsc{Tcc}.
Cite as

Axel Legay, Luca de Alfaro, and Marco Faella. An Introduction to the Tool Ticc. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{legay_et_al:OASIcs.TrustworthySW.2006.766,
  author =	{Legay, Axel and de Alfaro, Luca and Faella, Marco},
  title =	{{An Introduction to the Tool Ticc}},
  booktitle =	{Workshop on Trustworthy Software},
  pages =	{1--32},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.766},
  URN =		{urn:nbn:de:0030-drops-7667},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.766},
  annote =	{Keywords: Open system, game, interface automata}
}
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact