4 Search Results for "Bozga, Marius"

Document
DOI: 10.4230/LIPIcs.CONCUR.2022.24
On an Invariance Problem for Parameterized Concurrent Systems

Authors: Marius Bozga, Lucas Bueri, and Radu Iosif

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
We consider concurrent systems consisting of replicated finite-state processes that synchronize via joint interactions in a network with user-defined topology. The system is specified using a resource logic with a multiplicative connective and inductively defined predicates, reminiscent of Separation Logic [John C. Reynolds, 2002]. The problem we consider is if a given formula in this logic defines an invariant, namely whether any model of the formula, following an arbitrary firing sequence of interactions, is transformed into another model of the same formula. This property, called havoc invariance, is quintessential in proving the correctness of reconfiguration programs that change the structure of the network at runtime. We show that the havoc invariance problem is many-one reducible to the entailment problem ϕ ⊧ ψ, asking if any model of ϕ is also a model of ψ. Although, in general, havoc invariance is found to be undecidable, this reduction allows to prove that havoc invariance is in 2EXP, for a general fragment of the logic, with a 2EXP entailment problem.
Cite as

Marius Bozga, Lucas Bueri, and Radu Iosif. On an Invariance Problem for Parameterized Concurrent Systems. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bozga_et_al:LIPIcs.CONCUR.2022.24,
  author =	{Bozga, Marius and Bueri, Lucas and Iosif, Radu},
  title =	{{On an Invariance Problem for Parameterized Concurrent Systems}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{24:1--24:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.24},
  URN =		{urn:nbn:de:0030-drops-170874},
  doi =		{10.4230/LIPIcs.CONCUR.2022.24},
  annote =	{Keywords: parameterized verification, invariant checking, resource logics, reconfigurable systems, tree automata}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.33
Revisiting Parameter Synthesis for One-Counter Automata

Authors: Guillermo A. Pérez and Ritam Raha

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
We study the synthesis problem for one-counter automata with parameters. One-counter automata are obtained by extending classical finite-state automata with a counter whose value can range over non-negative integers and be tested for zero. The updates and tests applicable to the counter can further be made parametric by introducing a set of integer-valued variables called parameters. The synthesis problem for such automata asks whether there exists a valuation of the parameters such that all infinite runs of the automaton satisfy some ω-regular property. Lechner showed that (the complement of) the problem can be encoded in a restricted one-alternation fragment of Presburger arithmetic with divisibility. In this work (i) we argue that said fragment, called ∀∃_RPAD^+, is unfortunately undecidable. Nevertheless, by a careful re-encoding of the problem into a decidable restriction of ∀∃_RPAD^+, (ii) we prove that the synthesis problem is decidable in general and in 2NEXP for several fixed ω-regular properties. Finally, (iii) we give polynomial-space algorithms for the special cases of the problem where parameters can only be used in counter tests.
Cite as

Guillermo A. Pérez and Ritam Raha. Revisiting Parameter Synthesis for One-Counter Automata. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 33:1-33:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{perez_et_al:LIPIcs.CSL.2022.33,
  author =	{P\'{e}rez, Guillermo A. and Raha, Ritam},
  title =	{{Revisiting Parameter Synthesis for One-Counter Automata}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{33:1--33:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.33},
  URN =		{urn:nbn:de:0030-drops-157534},
  doi =		{10.4230/LIPIcs.CSL.2022.33},
  annote =	{Keywords: Parametric one-counter automata, Reachability, Software Verification}
}
Document
DOI: 10.4230/LITES-v006-i001-a001
Local Planning Semantics: A Semantics for Distributed Real-Time Systems

Authors: Mahieddine Dellabani, Jacques Combaz, Saddek Bensalem, and Marius Bozga

Published in: LITES, Volume 6, Issue 1 (2019). Leibniz Transactions on Embedded Systems, Volume 6, Issue 1

Abstract
Design, implementation and verification of distributed real-time systems are acknowledged to be very hard tasks. Such systems are prone to different kinds of delay, such as execution time of actions or communication delays implied by distributed platforms. The latter increase considerably the complexity of coordinating the parallel activities of running components. Scheduling such systems must cope with those delays by proposing execution strategies  ensuring global consistency while satisfying the imposed timing constraints. In this paper, we investigate a formal model for such systems as compositions of timed automata subject to multiparty interactions, and propose a semantics aiming to overcome the communication delays problem through anticipating the execution of interactions. To be effective in a distributed context, scheduling an interaction should rely on (as much as possible) local information only, namely the state of its participating components. However, as shown in this paper these information is not always sufficient and does not guarantee a safe execution of the system as it may introduce deadlocks. Moreover, delays may also affect the satisfaction of timing constraints, which also corresponds to deadlocks in the former model. Thus, we also explore methods for analyzing such deadlock situations and for computing  deadlock-free scheduling strategies when possible.
Cite as

Mahieddine Dellabani, Jacques Combaz, Saddek Bensalem, and Marius Bozga. Local Planning Semantics: A Semantics for Distributed Real-Time Systems. In LITES, Volume 6, Issue 1 (2019). Leibniz Transactions on Embedded Systems, Volume 6, Issue 1, pp. 01:1-01:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{dellabani_et_al:LITES-v006-i001-a001,
  author =	{Dellabani, Mahieddine and Combaz, Jacques and Bensalem, Saddek and Bozga, Marius},
  title =	{{Local Planning Semantics: A Semantics for Distributed Real-Time Systems}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{01:1--01:27},
  ISSN =	{2199-2002},
  year =	{2019},
  volume =	{6},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LITES-v006-i001-a001},
  doi =		{10.4230/LITES-v006-i001-a001},
  annote =	{Keywords: Distributed Real-Time Systems, Timed Automata, Formal Verification}
}
Document
DOI: 10.4230/DagSemProc.08331.5
Modeling Heterogeneous Real-time Components in BIP

Authors: Ananda Basu, Marius Bozga, and Joseph Sifakis

Published in: Dagstuhl Seminar Proceedings, Volume 8331, Perspectives Workshop: Model Engineering of Complex Systems (MECS) (2008)

Abstract
We present a methodology for modeling heterogeneous real-time components. Components are obtained as the superposition of three layers : Behavior, specified as a set of transitions; Interactions between transitions of the behavior; Priorities, used to choose amongst possible interactions. A parameterized binary composition operator is used to compose components layer by layer. We present the BIP language for the description and composition of layered components as well as associated tools for executing and analyzing components on a dedicated platform. The language provides a powerful mechanism for structuring interactions involving rendezvous and broadcast. We show that synchronous and timed systems are particular classes of components. Finally, we provide examples showing the utility of the BIP framework in heterogeneous component modeling.
Cite as

Ananda Basu, Marius Bozga, and Joseph Sifakis. Modeling Heterogeneous Real-time Components in BIP. In Perspectives Workshop: Model Engineering of Complex Systems (MECS). Dagstuhl Seminar Proceedings, Volume 8331, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{basu_et_al:DagSemProc.08331.5,
  author =	{Basu, Ananda and Bozga, Marius and Sifakis, Joseph},
  title =	{{Modeling Heterogeneous Real-time Components in BIP}},
  booktitle =	{Perspectives Workshop: Model Engineering of Complex Systems (MECS)},
  pages =	{1--10},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8331},
  editor =	{Uwe A{\ss}mann and Jean B\'{e}zivin and Richard Paige and Bernhard Rumpe and Douglas C. Schmidt},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.08331.5},
  URN =		{urn:nbn:de:0030-drops-16026},
  doi =		{10.4230/DagSemProc.08331.5},
  annote =	{Keywords: Component based construction, Heterogeneous systems, Modeling and simulation, Code generation}
}
  • Refine by Author
  • 3 Bozga, Marius
  • 1 Basu, Ananda
  • 1 Bensalem, Saddek
  • 1 Bueri, Lucas
  • 1 Combaz, Jacques
  • Show More...

  • Refine by Classification
  • 1 Software and its engineering → Formal software verification
  • 1 Theory of computation → Formal languages and automata theory
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Quantitative automata

  • Refine by Keyword
  • 1 Code generation
  • 1 Component based construction
  • 1 Distributed Real-Time Systems
  • 1 Formal Verification
  • 1 Heterogeneous systems
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2022
  • 1 2008
  • 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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact