7 Search Results for "Groote, Jan Friso"


Document
Real Equation Systems with Alternating Fixed-Points

Authors: Jan Friso Groote and Tim A. C. Willemse

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)


Abstract
We introduce the notion of a Real Equation System (RES), which lifts Boolean Equation Systems (BESs) to the domain of extended real numbers. Our RESs allow arbitrary nesting of least and greatest fixed-point operators. We show that each RES can be rewritten into an equivalent RES in normal form. These normal forms provide the basis for a complete procedure to solve RESs. This employs the elimination of the fixed-point variable at the left side of an equation from its right-hand side, combined with a technique often referred to as Gauß-elimination. We illustrate how this framework can be used to verify quantitative modal formulas with alternating fixed-point operators interpreted over probabilistic labelled transition systems.

Cite as

Jan Friso Groote and Tim A. C. Willemse. Real Equation Systems with Alternating Fixed-Points. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{groote_et_al:LIPIcs.CONCUR.2023.28,
  author =	{Groote, Jan Friso and Willemse, Tim A. C.},
  title =	{{Real Equation Systems with Alternating Fixed-Points}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{28:1--28:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.28},
  URN =		{urn:nbn:de:0030-drops-190225},
  doi =		{10.4230/LIPIcs.CONCUR.2023.28},
  annote =	{Keywords: Real Equation System, Solution method, Gau{\ss}-elimination, Model checking, Quantitative modal mu-calculus}
}
Document
Computing Minimal Distinguishing Hennessy-Milner Formulas is NP-Hard, but Variants are Tractable

Authors: Jan Martens and Jan Friso Groote

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)


Abstract
We study the problem of computing minimal distinguishing formulas for non-bisimilar states in finite LTSs. We show that this is NP-hard if the size of the formula must be minimal. Similarly, the existence of a short distinguishing trace is NP-complete. However, we can provide polynomial algorithms, if minimality is formulated as the minimal number of nested modalities, and it can even be extended by recursively requiring a minimal number of nested negations. A prototype implementation shows that the generated formulas are much smaller than those generated by the method introduced by Cleaveland.

Cite as

Jan Martens and Jan Friso Groote. Computing Minimal Distinguishing Hennessy-Milner Formulas is NP-Hard, but Variants are Tractable. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 32:1-32:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{martens_et_al:LIPIcs.CONCUR.2023.32,
  author =	{Martens, Jan and Groote, Jan Friso},
  title =	{{Computing Minimal Distinguishing Hennessy-Milner Formulas is NP-Hard, but Variants are Tractable}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{32:1--32:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.32},
  URN =		{urn:nbn:de:0030-drops-190268},
  doi =		{10.4230/LIPIcs.CONCUR.2023.32},
  annote =	{Keywords: Distinguishing behaviour, Hennessy-Milner logic, NP-hardness}
}
Document
Renamingless Capture-Avoiding Substitution for Definitional Interpreters

Authors: Casper Bach Poulsen

Published in: OASIcs, Volume 109, Eelco Visser Commemorative Symposium (EVCS 2023)


Abstract
Substitution is a common and popular approach to implementing name binding in definitional interpreters. A common pitfall of implementing substitution functions is variable capture. The traditional approach to avoiding variable capture is to rename variables. However, traditional renaming makes for an inefficient interpretation strategy. Furthermore, for applications where partially-interpreted terms are user facing it can be confusing if names in uninterpreted parts of the program have been changed. In this paper we explore two techniques for implementing capture avoiding substitution in definitional interpreters to avoid renaming.

Cite as

Casper Bach Poulsen. Renamingless Capture-Avoiding Substitution for Definitional Interpreters. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 2:1-2:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{bachpoulsen:OASIcs.EVCS.2023.2,
  author =	{Bach Poulsen, Casper},
  title =	{{Renamingless Capture-Avoiding Substitution for Definitional Interpreters}},
  booktitle =	{Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages =	{2:1--2:10},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-267-9},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{109},
  editor =	{L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.EVCS.2023.2},
  URN =		{urn:nbn:de:0030-drops-177728},
  doi =		{10.4230/OASIcs.EVCS.2023.2},
  annote =	{Keywords: Capture-avoiding substitution, lambda calculus, definitional interpreter}
}
Document
Bisimulation by Partitioning Is Ω((m+n)log n)

Authors: Jan Friso Groote, Jan Martens, and Erik de Vink

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)


Abstract
An asymptotic lowerbound of Ω((m+n)log n) is established for partition refinement algorithms that decide bisimilarity on labeled transition systems. The lowerbound is obtained by subsequently analysing two families of deterministic transition systems - one with a growing action set and another with a fixed action set. For deterministic transition systems with a one-letter action set, bisimilarity can be decided with fundamentally different techniques than partition refinement. In particular, Paige, Tarjan, and Bonic give a linear algorithm for this specific situation. We show, exploiting the concept of an oracle, that the approach of Paige, Tarjan, and Bonic is not of help to develop a generic algorithm for deciding bisimilarity on labeled transition systems that is faster than the established lowerbound of Ω((m+n)log n).

Cite as

Jan Friso Groote, Jan Martens, and Erik de Vink. Bisimulation by Partitioning Is Ω((m+n)log n). In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{groote_et_al:LIPIcs.CONCUR.2021.31,
  author =	{Groote, Jan Friso and Martens, Jan and de Vink, Erik},
  title =	{{Bisimulation by Partitioning Is \Omega((m+n)log n)}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{31:1--31:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.31},
  URN =		{urn:nbn:de:0030-drops-144087},
  doi =		{10.4230/LIPIcs.CONCUR.2021.31},
  annote =	{Keywords: Bisimilarity, partition refinement, labeled transition system, lowerbound}
}
Document
A Near-Linear-Time Algorithm for Weak Bisimilarity on Markov Chains

Authors: David N. Jansen, Jan Friso Groote, Ferry Timmers, and Pengfei Yang

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)


Abstract
This article improves the time bound for calculating the weak/branching bisimulation minimisation quotient on state-labelled discrete-time Markov chains from O(m n) to an expected-time O(m log⁴ n), where n is the number of states and m the number of transitions. For these results we assume that the set of state labels AP is small (|AP| ∈ O(m/n log⁴ n)). It follows the ideas of Groote et al. (ACM ToCL 2017) in combination with an efficient algorithm to handle decremental strongly connected components (Bernstein et al., STOC 2019).

Cite as

David N. Jansen, Jan Friso Groote, Ferry Timmers, and Pengfei Yang. A Near-Linear-Time Algorithm for Weak Bisimilarity on Markov Chains. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{jansen_et_al:LIPIcs.CONCUR.2020.8,
  author =	{Jansen, David N. and Groote, Jan Friso and Timmers, Ferry and Yang, Pengfei},
  title =	{{A Near-Linear-Time Algorithm for Weak Bisimilarity on Markov Chains}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.8},
  URN =		{urn:nbn:de:0030-drops-128209},
  doi =		{10.4230/LIPIcs.CONCUR.2020.8},
  annote =	{Keywords: Behavioural Equivalence, weak Bisimulation, Markov Chain}
}
Document
Adaptive Non-Linear Pattern Matching Automata

Authors: Rick Erkens and Maurice Laveaux

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)


Abstract
Efficient pattern matching is fundamental for practical term rewrite engines. By preprocessing the given patterns into a finite deterministic automaton the matching patterns can be decided in a single traversal of the relevant parts of the input term. Most automaton-based techniques are restricted to linear patterns, where each variable occurs at most once, and require an additional post-processing step to check so-called variable consistency. However, we can show that interleaving the variable consistency and pattern matching phases can reduce the number of required steps to find a match all matches. Therefore, we take the existing adaptive pattern matching automata as introduced by Sekar et al and extend it these with consistency checks. We prove that the resulting deterministic pattern matching automaton is correct, and show that its evaluation depth is can be shorter than two-phase approaches.

Cite as

Rick Erkens and Maurice Laveaux. Adaptive Non-Linear Pattern Matching Automata. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 20:1-20:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{erkens_et_al:LIPIcs.FSCD.2020.20,
  author =	{Erkens, Rick and Laveaux, Maurice},
  title =	{{Adaptive Non-Linear Pattern Matching Automata}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{20:1--20:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.20},
  URN =		{urn:nbn:de:0030-drops-123427},
  doi =		{10.4230/LIPIcs.FSCD.2020.20},
  annote =	{Keywords: Pattern matching, Term indexing, Tree automata}
}
Document
The Formal Specification Language mCRL2

Authors: Jan Friso Groote, Aad Mathijssen, Michel Reniers, Yaroslav Usenko, and Muck van Weerdenburg

Published in: Dagstuhl Seminar Proceedings, Volume 6351, Methods for Modelling Software Systems (MMOSS) (2007)


Abstract
We introduce mCRL2, a specification language that can be used to specify and analyse the behaviour of distributed systems. This language is the successor of the mCRL specification language. The mCRL2 language extends a timed basic process algebra with the possibility to define and use abstract data types. The mCRL2 data language features predefined and higher-order data types. The process algebraic part of mCRL2 allows a faithful translation of coloured Petri nets and component based systems: we have introduced multiactions and we have separated communication and parallelism.

Cite as

Jan Friso Groote, Aad Mathijssen, Michel Reniers, Yaroslav Usenko, and Muck van Weerdenburg. The Formal Specification Language mCRL2. In Methods for Modelling Software Systems (MMOSS). Dagstuhl Seminar Proceedings, Volume 6351, pp. 1-34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{groote_et_al:DagSemProc.06351.12,
  author =	{Groote, Jan Friso and Mathijssen, Aad and Reniers, Michel and Usenko, Yaroslav and van Weerdenburg, Muck},
  title =	{{The Formal Specification Language mCRL2}},
  booktitle =	{Methods for Modelling Software Systems (MMOSS)},
  pages =	{1--34},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6351},
  editor =	{Ed Brinksma and David Harel and Angelika Mader and Perdita Stevens and Roel Wieringa},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06351.12},
  URN =		{urn:nbn:de:0030-drops-8626},
  doi =		{10.4230/DagSemProc.06351.12},
  annote =	{Keywords: Specification language, abstract data types, process algebra, operational semantics}
}
  • Refine by Author
  • 5 Groote, Jan Friso
  • 2 Martens, Jan
  • 1 Bach Poulsen, Casper
  • 1 Erkens, Rick
  • 1 Jansen, David N.
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Modal and temporal logics
  • 1 Software and its engineering → Formal software verification
  • 1 Software and its engineering → Semantics
  • 1 Theory of computation
  • 1 Theory of computation → Design and analysis of algorithms
  • Show More...

  • Refine by Keyword
  • 1 Behavioural Equivalence
  • 1 Bisimilarity
  • 1 Capture-avoiding substitution
  • 1 Distinguishing behaviour
  • 1 Gauß-elimination
  • Show More...

  • Refine by Type
  • 7 document

  • Refine by Publication Year
  • 3 2023
  • 2 2020
  • 1 2007
  • 1 2021

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