5 Search Results for "Degorre, Aldric"

Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.14
Regulating Synchronous Data Exchange to Meet Control Flow and Data Specifications

Authors: Ashwin Bhaskar and M. Praveen

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

Abstract
When multiple software components interact via method calls, we may want to ensure that the order of invoked methods and the arguments provided adhere to some specification. The classic problem associated with interface automata checks for the existence of a mediator whose intention is to act as a buffer in between method invocations so that invocations do not go unanswered. We extend the base model underlying interface automata, enabling them to exchange integer values - one automaton generates an integer value and outputs it by firing a generating transition and another automaton receives the value by synchronously firing a receiving transition. Transitions in the automata can have guards with linear order constraints on the exchanged values, influencing which methods can or can not be invoked later. So the generated values influence the sequences of invocations that are enabled. We specify desirable properties of the sequence of method calls and the arguments passed to them using an extension of Linear Temporal Logic (LTL). We consider the interoperability problem, which is to check if it is possible to generate integer values in such a way that all enabled sequences satisfy the given specification. We show that the interoperability problem is undecidable in general, even when there are only two participating automata. We show decidability in the case where guards on generating transitions can only have equality constraints on the exchanged value (but receiving transitions can continue to have linear order constraints). We model this problem as a game between two players, one trying to generate integer values such that violating sequences are disabled while the other player tries to dig out violating sequences that are enabled. Interoperability is equivalent to the first player having a winning strategy. We solve this game via a finite abstraction, which results in a symbolic game. We then show that winning strategies for the symbolic game can be translated to winning strategies for the original game over integers.
Cite as

Ashwin Bhaskar and M. Praveen. Regulating Synchronous Data Exchange to Meet Control Flow and Data Specifications. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bhaskar_et_al:LIPIcs.FSTTCS.2025.14,
  author =	{Bhaskar, Ashwin and Praveen, M.},
  title =	{{Regulating Synchronous Data Exchange to Meet Control Flow and Data Specifications}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{14:1--14:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.14},
  URN =		{urn:nbn:de:0030-drops-250962},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.14},
  annote =	{Keywords: Distributed Systems, Interface Automata, Registers, Parity Games}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.21
Quantitative Language Automata

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

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
A quantitative word automaton (QWA) defines a function from infinite words to values. For example, every infinite run of a limit-average QWA 𝒜 obtains a mean payoff, and every word w ∈ Σ^ω is assigned the maximal mean payoff obtained by nondeterministic runs of 𝒜 over w. We introduce quantitative language automata (QLAs) that define functions from language generators (i.e., implementations) to values, where a language generator can be nonprobabilistic, defining a set of infinite words, or probabilistic, defining a probability measure over infinite words. A QLA consists of a QWA and an aggregator function. For example, given a QWA 𝒜, the infimum aggregator maps each language L ⊆ Σ^ω to the greatest lower bound assigned by 𝒜 to any word in L. For boolean value sets, QWAs define boolean properties of traces, and QLAs define boolean properties of sets of traces, i.e., hyperproperties. For more general value sets, QLAs serve as a specification language for a generalization of hyperproperties, called quantitative hyperproperties. A nonprobabilistic (resp. probabilistic) quantitative hyperproperty assigns a value to each set (resp. distribution) G of traces, e.g., the minimal (resp. expected) average response time exhibited by the traces in G. We give several examples of quantitative hyperproperties and investigate three paradigmatic problems for QLAs: evaluation, nonemptiness, and universality. In the evaluation problem, given a QLA 𝔸 and an implementation G, we ask for the value that 𝔸 assigns to G. In the nonemptiness (resp. universality) problem, given a QLA 𝔸 and a value k, we ask whether 𝔸 assigns at least k to some (resp. every) language. We provide a comprehensive picture of decidability for these problems for QLAs with common aggregators as well as their restrictions to ω-regular languages and trace distributions generated by finite-state Markov chains.
Cite as

Thomas A. Henzinger, Pavol Kebis, Nicolas Mazzocchi, and N. Ege Saraç. Quantitative Language Automata. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 21:1-21:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{henzinger_et_al:LIPIcs.CONCUR.2025.21,
  author =	{Henzinger, Thomas A. and Kebis, Pavol and Mazzocchi, Nicolas and Sara\c{c}, N. Ege},
  title =	{{Quantitative Language Automata}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{21:1--21:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.21},
  URN =		{urn:nbn:de:0030-drops-239718},
  doi =		{10.4230/LIPIcs.CONCUR.2025.21},
  annote =	{Keywords: Quantitative hyperproperties, quantitative automata, automata-based verification}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2023.10
Bandwidth of Timed Automata: 3 Classes

Authors: Eugene Asarin, Aldric Degorre, Cătălin Dima, and Bernardo Jacobo Inclán

Published in: LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)

Abstract
Timed languages contain sequences of discrete events ("letters") separated by real-valued delays, they can be recognized by timed automata, and represent behaviors of various real-time systems. The notion of bandwidth of a timed language defined in [Jacobo Inclán et al., 2022] characterizes the amount of information per time unit, encoded in words of the language observed with some precision ε. In this paper, we identify three classes of timed automata according to the asymptotics of the bandwidth of their languages with respect to this precision ε: automata are either meager, with an O(1) bandwidth, normal, with a Θ(log(1/ε)) bandwidth, or obese, with Θ(1/ε) bandwidth. We define two structural criteria and prove that they partition timed automata into these 3 classes of bandwidth, implying that there are no intermediate asymptotic classes. The classification problem of a timed automaton is PSPACE-complete. Both criteria are formulated using morphisms from paths of the timed automaton to some finite monoids extending Puri’s orbit graphs; the proofs are based on Simon’s factorization forest theorem.
Cite as

Eugene Asarin, Aldric Degorre, Cătălin Dima, and Bernardo Jacobo Inclán. Bandwidth of Timed Automata: 3 Classes. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{asarin_et_al:LIPIcs.FSTTCS.2023.10,
  author =	{Asarin, Eugene and Degorre, Aldric and Dima, C\u{a}t\u{a}lin and Jacobo Incl\'{a}n, Bernardo},
  title =	{{Bandwidth of Timed Automata: 3 Classes}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{10:1--10:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.10},
  URN =		{urn:nbn:de:0030-drops-193838},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.10},
  annote =	{Keywords: timed automata, information theory, bandwidth, entropy, orbit graphs, factorization forests}
}
Document
DOI: 10.4230/LIPIcs.STACS.2016.11
Entropy Games and Matrix Multiplication Games

Authors: Eugene Asarin, Julien Cervelle, Aldric Degorre, Catalin Dima, Florian Horn, and Victor Kozyakin

Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

Abstract
Two intimately related new classes of games are introduced and studied: entropy games (EGs) and matrix multiplication games (MMGs). An EG is played on a finite arena by two-and-a-half players: Despot, Tribune and the non-deterministic People. Despot wants to make the set of possible People's behaviors as small as possible, while Tribune wants to make it as large as possible. An MMG is played by two players that alternately write matrices from some predefined finite sets. One wants to maximize the growth rate of the product, and the other to minimize it. We show that in general MMGs are undecidable in quite a strong sense. On the positive side, EGs correspond to a subclass of MMGs, and we prove that such MMGs and EGs are determined, and that the optimal strategies are simple. The complexity of solving such games is in NP cap coNP.
Cite as

Eugene Asarin, Julien Cervelle, Aldric Degorre, Catalin Dima, Florian Horn, and Victor Kozyakin. Entropy Games and Matrix Multiplication Games. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 11:1-11:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{asarin_et_al:LIPIcs.STACS.2016.11,
  author =	{Asarin, Eugene and Cervelle, Julien and Degorre, Aldric and Dima, Catalin and Horn, Florian and Kozyakin, Victor},
  title =	{{Entropy Games and Matrix Multiplication Games}},
  booktitle =	{33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
  pages =	{11:1--11:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-001-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{47},
  editor =	{Ollinger, Nicolas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.11},
  URN =		{urn:nbn:de:0030-drops-57129},
  doi =		{10.4230/LIPIcs.STACS.2016.11},
  annote =	{Keywords: game theory, entropy, joint spectral radius}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.376
Two Size Measures for Timed Languages

Authors: Eugene Asarin and Aldric Degorre

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

Abstract
Quantitative properties of timed regular languages, such as information content (growth rate, entropy) are explored. The approach suggested by the same authors is extended to languages of timed automata with punctual (equalities) and non-punctual (non-equalities) transition guards. Two size measures for such languages are identified: mean dimension and volumetric entropy. The former is the linear growth rate of the dimension of the language; it is characterized as the spectral radius of a max-plus matrix associated to the automaton. The latter is the exponential growth rate of the volume of the language; it is characterized as the logarithm of the spectral radius of a matrix integral operator on some Banach space associated to the automaton. Relation of the two size measures to classical information-theoretic concepts is explored.
Cite as

Eugene Asarin and Aldric Degorre. Two Size Measures for Timed Languages. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 376-387, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{asarin_et_al:LIPIcs.FSTTCS.2010.376,
  author =	{Asarin, Eugene and Degorre, Aldric},
  title =	{{Two Size Measures for Timed Languages}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{376--387},
  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.376},
  URN =		{urn:nbn:de:0030-drops-28793},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.376},
  annote =	{Keywords: timed automata, entropy, mean dimension}
}
  • Refine by Type
  • 5 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 2 2025
  • 1 2023
  • 1 2016
  • 1 2010

  • Refine by Author
  • 3 Asarin, Eugene
  • 3 Degorre, Aldric
  • 1 Bhaskar, Ashwin
  • 1 Cervelle, Julien
  • 1 Dima, Catalin
  • Show More...

  • Refine by Series/Journal
  • 5 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Quantitative automata
  • 1 Theory of computation → Automata over infinite objects
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Modal and temporal logics
  • 1 Theory of computation → Timed and hybrid models
  • Show More...

  • Refine by Keyword
  • 3 entropy
  • 2 timed automata
  • 1 Distributed Systems
  • 1 Interface Automata
  • 1 Parity Games
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact