6 Search Results for "Larsen, Kim Guldstrand"

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-dev.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/OASIcs.SynCoP.2015.77
Parametric Verification of Weighted Systems

Authors: Peter Christoffersen, Mikkel Hansen, Anders Mariegaard, Julian Trier Ringsmose, Kim Guldstrand Larsen, and Radu Mardare

Published in: OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015)

Abstract
This paper addresses the problem of parametric model checking for weighted transition systems. We consider transition systems labelled with linear equations over a set of parameters and we use them to provide semantics for a parametric version of weighted CTL where the until and next operators are themselves indexed with linear equations. The parameters change the model-checking problem into a problem of computing a linear system of inequalities that characterizes the parameters that guarantee the satisfiability. To address this problem, we use parametric dependency graphs (PDGs) and we propose a global update function that yields an assignment to each node in a PDG. For an iterative application of the function, we prove that a fixed point assignment to PDG nodes exists and the set of assignments constitutes a well-quasi ordering, thus ensuring that the fixed point assignment can be found after finitely many iterations. To demonstrate the utility of our technique, we have implemented a prototype tool that computes the constraints on parameters for model checking problems.
Cite as

Peter Christoffersen, Mikkel Hansen, Anders Mariegaard, Julian Trier Ringsmose, Kim Guldstrand Larsen, and Radu Mardare. Parametric Verification of Weighted Systems. In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 77-90, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{christoffersen_et_al:OASIcs.SynCoP.2015.77,
  author =	{Christoffersen, Peter and Hansen, Mikkel and Mariegaard, Anders and Ringsmose, Julian Trier and Larsen, Kim Guldstrand and Mardare, Radu},
  title =	{{Parametric Verification of Weighted Systems}},
  booktitle =	{2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
  pages =	{77--90},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.77},
  URN =		{urn:nbn:de:0030-drops-56115},
  doi =		{10.4230/OASIcs.SynCoP.2015.77},
  annote =	{Keywords: parametric weighted transition systems, parametric weighted CTL, parametric model checking, well-quasi ordering, tool}
}
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-dev.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}
}
Document
DOI: 10.4230/OASIcs.WCET.2010.113
METAMOC: Modular Execution Time Analysis using Model Checking

Authors: Andreas E. Dalsgaard, Mads Chr. Olesen, Martin Toft, René Rydhof Hansen, and Kim Guldstrand Larsen

Published in: OASIcs, Volume 15, 10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010)

Abstract
Safe and tight worst-case execution times (WCETs) are important when scheduling hard real-time systems. This paper presents METAMOC, a modular method, based on model checking and static analysis, that determines safe and tight WCETs for programs running on platforms featuring caching and pipelining. The method works by constructing a UPPAAL model of the program being analysed and annotating the model with information from an inter-procedural value analysis. The program model is then combined with a model of the hardware platform and model checked for the WCET. Through support for the platforms ARM7, ARM9 and ATMEL AVR 8-bit, the modularity and retargetability of the method are demonstrated, as only the pipeline needs to be remodelled. Hardware modelling is performed in a state-of-the-art graphical modelling environment. Experiments on the Mälardalen WCET benchmark programs show that taking caching into account yields much tighter WCETs than without modelling caches, and that METAMOC is a sufficiently fast and versatile approach for WCET analysis.
Cite as

Andreas E. Dalsgaard, Mads Chr. Olesen, Martin Toft, René Rydhof Hansen, and Kim Guldstrand Larsen. METAMOC: Modular Execution Time Analysis using Model Checking. In 10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010). Open Access Series in Informatics (OASIcs), Volume 15, pp. 113-123, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{dalsgaard_et_al:OASIcs.WCET.2010.113,
  author =	{Dalsgaard, Andreas E. and Olesen, Mads Chr. and Toft, Martin and Hansen, Ren\'{e} Rydhof and Larsen, Kim Guldstrand},
  title =	{{METAMOC: Modular Execution Time Analysis using Model Checking}},
  booktitle =	{10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010)},
  pages =	{113--123},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-21-7},
  ISSN =	{2190-6807},
  year =	{2010},
  volume =	{15},
  editor =	{Lisper, Bj\"{o}rn},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2010.113},
  URN =		{urn:nbn:de:0030-drops-28319},
  doi =		{10.4230/OASIcs.WCET.2010.113},
  annote =	{Keywords: WCET analysis, timed automata, model checking, UPPAAL}
}
Document
DOI: 10.4230/DagSemProc.10031.1
10031 Abstracts Collection – Quantitative Models: Expressiveness and Analysis

Authors: Christel Baier, Manfred Droste, Paul Gastin, and Kim Guldstrand Larsen

Published in: Dagstuhl Seminar Proceedings, Volume 10031, Quantitative Models: Expressiveness and Analysis (2010)

Abstract
From Jan 18 to Jan 22, 2010, the Dagstuhl Seminar 10031 ``Quantitative Models: Expressiveness and Analysis '' 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

Christel Baier, Manfred Droste, Paul Gastin, and Kim Guldstrand Larsen. 10031 Abstracts Collection – Quantitative Models: Expressiveness and Analysis. In Quantitative Models: Expressiveness and Analysis. Dagstuhl Seminar Proceedings, Volume 10031, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{baier_et_al:DagSemProc.10031.1,
  author =	{Baier, Christel and Droste, Manfred and Gastin, Paul and Larsen, Kim Guldstrand},
  title =	{{10031 Abstracts Collection – Quantitative Models: Expressiveness and Analysis}},
  booktitle =	{Quantitative Models: Expressiveness and Analysis},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10031},
  editor =	{Christel Baier and Manfred Droste and Paul Gastin and Kim Guldstrand Larsen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10031.1},
  URN =		{urn:nbn:de:0030-drops-26839},
  doi =		{10.4230/DagSemProc.10031.1},
  annote =	{Keywords: Quantitative models, quantitative analysis, timed and hybrid systems, probabilistic systems, weighted automata}
}
Document
DOI: 10.4230/DagSemProc.10031.2
10031 Executive Summary – Quantitative Models: Expressiveness and Analysis

Authors: Christel Baier, Manfred Droste, Paul Gastin, and Kim Guldstrand Larsen

Published in: Dagstuhl Seminar Proceedings, Volume 10031, Quantitative Models: Expressiveness and Analysis (2010)

Abstract
Quantitative models and quantitative analysis in Computer Science are currently intensively studied, resulting in a revision of the foundation of Computer Science where classical yes/no answers are replaced by quantitative analyses. The potential application areas are huge, e.g., performance analysis, operational research or embedded systems. The aim of the seminar was to address three fundamental topics which are closely related: quantitative analysis of real-time and hybrid systems; probabilistic analysis and stochastic automata; weighted automata. These three areas of research have mainly evolved independently so far and the relationship between them has emerged only recently. The seminar brought together leading researchers of the three areas, with the goal of future highly productive cross-fertilizations.
Cite as

Christel Baier, Manfred Droste, Paul Gastin, and Kim Guldstrand Larsen. 10031 Executive Summary – Quantitative Models: Expressiveness and Analysis. In Quantitative Models: Expressiveness and Analysis. Dagstuhl Seminar Proceedings, Volume 10031, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{baier_et_al:DagSemProc.10031.2,
  author =	{Baier, Christel and Droste, Manfred and Gastin, Paul and Larsen, Kim Guldstrand},
  title =	{{10031 Executive Summary – Quantitative Models: Expressiveness and Analysis}},
  booktitle =	{Quantitative Models: Expressiveness and Analysis},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10031},
  editor =	{Christel Baier and Manfred Droste and Paul Gastin and Kim Guldstrand Larsen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10031.2},
  URN =		{urn:nbn:de:0030-drops-26824},
  doi =		{10.4230/DagSemProc.10031.2},
  annote =	{Keywords: Quantitative models, quantitative analysis, timed and hybrid systems, probabilistic systems, weighted automata}
}
  • Refine by Author
  • 5 Larsen, Kim Guldstrand
  • 2 Baier, Christel
  • 2 Droste, Manfred
  • 2 Gastin, Paul
  • 1 Bønneland, Frederik Meyer
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Algorithmic game theory

  • Refine by Keyword
  • 3 weighted automata
  • 2 Quantitative models
  • 2 probabilistic systems
  • 2 quantitative analysis
  • 2 timed and hybrid systems
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 3 2010
  • 2 2015
  • 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