Search Results

Documents authored by Srba, Jiří

Found 2 Possible Name Variants:

Srba, Jiri

Document
Invited Talk
DOI: 10.4230/LIPIcs.CONCUR.2025.3
On-The-Fly Verification: Advancements in Dependency Graphs (Invited Talk)

Authors: Jiří Srba

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

Abstract
Dependency graphs have emerged as a versatile and powerful formalism with wide-ranging applications in formal verification. In this extended abstract, we provide an overview of selected advancements in on-the-fly verification techniques based on dependency graphs, focusing on the recent developments, optimizations and generalizations of this generic verification framework.
Cite as

Jiří Srba. On-The-Fly Verification: Advancements in Dependency Graphs (Invited Talk). In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 3:1-3:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{srba:LIPIcs.CONCUR.2025.3,
  author =	{Srba, Ji\v{r}{\'\i}},
  title =	{{On-The-Fly Verification: Advancements in Dependency Graphs}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{3:1--3:5},
  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.3},
  URN =		{urn:nbn:de:0030-drops-239534},
  doi =		{10.4230/LIPIcs.CONCUR.2025.3},
  annote =	{Keywords: dependency graphs, Boolean equation systems, on-the-fly algorithms, fixed-point computation, applications}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.25
On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions

Authors: Nicolaj Ø. Jensen, Kim G. Larsen, Didier Lime, and Jiří Srba

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

Abstract
Verification of real-time systems with multiple components controlled by multiple parties is a challenging task due to its computational complexity. We present an on-the-fly algorithm for verifying timed alternating-time temporal logic (TATL), a branching-time logic with quantifiers over outcomes that results from coalitions of players in such systems. We combine existing work on games and timed CTL verification in the abstract dependency graph (ADG) framework, which allows for easy creation of on-the-fly algorithms that only explore the state space as needed. In addition, we generalize the conventional inclusion check to the ADG framework which enables dynamic reductions of the dependency graph. Using the insights from the generalization, we present a novel abstraction that eliminates the need for inclusion checking altogether in our domain. We implement our algorithms in Uppaal and our experiments show that while inclusion checking considerably enhances performance, our abstraction provides even more significant improvements, almost two orders of magnitude faster than the naive method. In addition, we outperform Uppaal Tiga, which can verify only a strict subset of TATL. After implementing our new abstraction in Uppaal Tiga, we also improve its performance by almost an order of magnitude.
Cite as

Nicolaj Ø. Jensen, Kim G. Larsen, Didier Lime, and Jiří Srba. On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{jensen_et_al:LIPIcs.CONCUR.2025.25,
  author =	{Jensen, Nicolaj {\O}. and Larsen, Kim G. and Lime, Didier and Srba, Ji\v{r}{\'\i}},
  title =	{{On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{25:1--25:19},
  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.25},
  URN =		{urn:nbn:de:0030-drops-239756},
  doi =		{10.4230/LIPIcs.CONCUR.2025.25},
  annote =	{Keywords: Timed ATL, Symbolic Algorithms, Dependency Graphs, Timed Games}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.23
Partial Order Reduction for Reachability Games

Authors: Frederik Meyer Bønneland, Peter Gjøl Jensen, Kim G. Larsen, Marco Muñiz, and Jiří Srba

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

Abstract
Partial order reductions have been successfully applied to model checking of concurrent systems and practical applications of the technique show nontrivial reduction in the size of the explored state space. We present a theory of partial order reduction based on stubborn sets in the game-theoretical setting of 2-player games with reachability/safety objectives. Our stubborn reduction allows us to prune the interleaving behaviour of both players in the game, and we formally prove its correctness on the class of games played on general labelled transition systems. We then instantiate the framework to the class of weighted Petri net games with inhibitor arcs and provide its efficient implementation in the model checker TAPAAL. Finally, we evaluate our stubborn reduction on several case studies and demonstrate its efficiency.
Cite as

Frederik Meyer Bønneland, Peter Gjøl Jensen, Kim G. Larsen, Marco Muñiz, and Jiří Srba. Partial Order Reduction for Reachability Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 23:1-23:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bnneland_et_al:LIPIcs.CONCUR.2019.23,
  author =	{B{\o}nneland, Frederik Meyer and Jensen, Peter Gj{\o}l and Larsen, Kim G. and Mu\~{n}iz, Marco and Srba, Ji\v{r}{\'\i}},
  title =	{{Partial Order Reduction for Reachability Games}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{23:1--23:15},
  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.23},
  URN =		{urn:nbn:de:0030-drops-109251},
  doi =		{10.4230/LIPIcs.CONCUR.2019.23},
  annote =	{Keywords: Petri nets, games, synthesis, partial order reduction, stubborn sets}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.142
Polynomial Time Decidability of Weighted Synchronization under Partial Observability

Authors: Jan Kretinsky, Kim Guldstrand Larsen, Simon Laursen, and Jiri Srba

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
We consider weighted automata with both positive and negative integer weights on edges and study the problem of synchronization using adaptive strategies that may only observe whether the current weight-level is negative or nonnegative. We show that the synchronization problem is decidable in polynomial time for deterministic weighted automata.
Cite as

Jan Kretinsky, Kim Guldstrand Larsen, Simon Laursen, and Jiri Srba. Polynomial Time Decidability of Weighted Synchronization under Partial Observability. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 142-154, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{kretinsky_et_al:LIPIcs.CONCUR.2015.142,
  author =	{Kretinsky, Jan and Larsen, Kim Guldstrand and Laursen, Simon and Srba, Jiri},
  title =	{{Polynomial Time Decidability of Weighted Synchronization under Partial Observability}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{142--154},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.142},
  URN =		{urn:nbn:de:0030-drops-53927},
  doi =		{10.4230/LIPIcs.CONCUR.2015.142},
  annote =	{Keywords: weighted automata, partial observability, synchronization, complexity}
}

Srba, Jiří

Document
Invited Talk
DOI: 10.4230/LIPIcs.CONCUR.2025.3
On-The-Fly Verification: Advancements in Dependency Graphs (Invited Talk)

Authors: Jiří Srba

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

Abstract
Dependency graphs have emerged as a versatile and powerful formalism with wide-ranging applications in formal verification. In this extended abstract, we provide an overview of selected advancements in on-the-fly verification techniques based on dependency graphs, focusing on the recent developments, optimizations and generalizations of this generic verification framework.
Cite as

Jiří Srba. On-The-Fly Verification: Advancements in Dependency Graphs (Invited Talk). In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 3:1-3:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{srba:LIPIcs.CONCUR.2025.3,
  author =	{Srba, Ji\v{r}{\'\i}},
  title =	{{On-The-Fly Verification: Advancements in Dependency Graphs}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{3:1--3:5},
  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.3},
  URN =		{urn:nbn:de:0030-drops-239534},
  doi =		{10.4230/LIPIcs.CONCUR.2025.3},
  annote =	{Keywords: dependency graphs, Boolean equation systems, on-the-fly algorithms, fixed-point computation, applications}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.25
On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions

Authors: Nicolaj Ø. Jensen, Kim G. Larsen, Didier Lime, and Jiří Srba

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

Abstract
Verification of real-time systems with multiple components controlled by multiple parties is a challenging task due to its computational complexity. We present an on-the-fly algorithm for verifying timed alternating-time temporal logic (TATL), a branching-time logic with quantifiers over outcomes that results from coalitions of players in such systems. We combine existing work on games and timed CTL verification in the abstract dependency graph (ADG) framework, which allows for easy creation of on-the-fly algorithms that only explore the state space as needed. In addition, we generalize the conventional inclusion check to the ADG framework which enables dynamic reductions of the dependency graph. Using the insights from the generalization, we present a novel abstraction that eliminates the need for inclusion checking altogether in our domain. We implement our algorithms in Uppaal and our experiments show that while inclusion checking considerably enhances performance, our abstraction provides even more significant improvements, almost two orders of magnitude faster than the naive method. In addition, we outperform Uppaal Tiga, which can verify only a strict subset of TATL. After implementing our new abstraction in Uppaal Tiga, we also improve its performance by almost an order of magnitude.
Cite as

Nicolaj Ø. Jensen, Kim G. Larsen, Didier Lime, and Jiří Srba. On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{jensen_et_al:LIPIcs.CONCUR.2025.25,
  author =	{Jensen, Nicolaj {\O}. and Larsen, Kim G. and Lime, Didier and Srba, Ji\v{r}{\'\i}},
  title =	{{On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{25:1--25:19},
  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.25},
  URN =		{urn:nbn:de:0030-drops-239756},
  doi =		{10.4230/LIPIcs.CONCUR.2025.25},
  annote =	{Keywords: Timed ATL, Symbolic Algorithms, Dependency Graphs, Timed Games}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.23
Partial Order Reduction for Reachability Games

Authors: Frederik Meyer Bønneland, Peter Gjøl Jensen, Kim G. Larsen, Marco Muñiz, and Jiří Srba

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

Abstract
Partial order reductions have been successfully applied to model checking of concurrent systems and practical applications of the technique show nontrivial reduction in the size of the explored state space. We present a theory of partial order reduction based on stubborn sets in the game-theoretical setting of 2-player games with reachability/safety objectives. Our stubborn reduction allows us to prune the interleaving behaviour of both players in the game, and we formally prove its correctness on the class of games played on general labelled transition systems. We then instantiate the framework to the class of weighted Petri net games with inhibitor arcs and provide its efficient implementation in the model checker TAPAAL. Finally, we evaluate our stubborn reduction on several case studies and demonstrate its efficiency.
Cite as

Frederik Meyer Bønneland, Peter Gjøl Jensen, Kim G. Larsen, Marco Muñiz, and Jiří Srba. Partial Order Reduction for Reachability Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 23:1-23:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bnneland_et_al:LIPIcs.CONCUR.2019.23,
  author =	{B{\o}nneland, Frederik Meyer and Jensen, Peter Gj{\o}l and Larsen, Kim G. and Mu\~{n}iz, Marco and Srba, Ji\v{r}{\'\i}},
  title =	{{Partial Order Reduction for Reachability Games}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{23:1--23:15},
  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.23},
  URN =		{urn:nbn:de:0030-drops-109251},
  doi =		{10.4230/LIPIcs.CONCUR.2019.23},
  annote =	{Keywords: Petri nets, games, synthesis, partial order reduction, stubborn sets}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.142
Polynomial Time Decidability of Weighted Synchronization under Partial Observability

Authors: Jan Kretinsky, Kim Guldstrand Larsen, Simon Laursen, and Jiri Srba

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
We consider weighted automata with both positive and negative integer weights on edges and study the problem of synchronization using adaptive strategies that may only observe whether the current weight-level is negative or nonnegative. We show that the synchronization problem is decidable in polynomial time for deterministic weighted automata.
Cite as

Jan Kretinsky, Kim Guldstrand Larsen, Simon Laursen, and Jiri Srba. Polynomial Time Decidability of Weighted Synchronization under Partial Observability. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 142-154, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{kretinsky_et_al:LIPIcs.CONCUR.2015.142,
  author =	{Kretinsky, Jan and Larsen, Kim Guldstrand and Laursen, Simon and Srba, Jiri},
  title =	{{Polynomial Time Decidability of Weighted Synchronization under Partial Observability}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{142--154},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.142},
  URN =		{urn:nbn:de:0030-drops-53927},
  doi =		{10.4230/LIPIcs.CONCUR.2015.142},
  annote =	{Keywords: weighted automata, partial observability, synchronization, complexity}
}
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact