8 Search Results for "Groote, Jan Friso"

Document
DOI: 10.4230/LIPIcs.FSCD.2024.8
Mechanized Subject Expansion in Uniform Intersection Types for Perpetual Reductions

Authors: Andrej Dudenhefner and Daniele Pautasso

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
We provide a new, purely syntactical proof of strong normalization for the simply typed λ-calculus. The result relies on a novel proof of the equivalence between typability in the simple type system and typability in the uniform intersection type system (a restriction of the non-idempotent intersection type system). For formal verification, the equivalence is mechanized using the Coq proof assistant. In the present work, strong normalization of a given simply typed term M is shown in four steps. First, M is reduced to a normal form N via a suitable reduction strategy with a decreasing measure. Second, a uniform intersection type for the normal form N is inferred. Third, a uniform intersection type for M is constructed iteratively via subject expansion. Fourth, strong normalization of M is shown by induction on the size of the type derivation. A supplementary contribution is a family of perpetual reduction strategies, i.e. strategies which preserve infinite reduction paths. This family allows for subject expansion in the intersection type systems of interest, and contains a reduction strategy with a decreasing measure in the simple type system. A notable member of this family is Barendregt’s F_∞ reduction strategy.
Cite as

Andrej Dudenhefner and Daniele Pautasso. Mechanized Subject Expansion in Uniform Intersection Types for Perpetual Reductions. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{dudenhefner_et_al:LIPIcs.FSCD.2024.8,
  author =	{Dudenhefner, Andrej and Pautasso, Daniele},
  title =	{{Mechanized Subject Expansion in Uniform Intersection Types for Perpetual Reductions}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.8},
  URN =		{urn:nbn:de:0030-drops-203371},
  doi =		{10.4230/LIPIcs.FSCD.2024.8},
  annote =	{Keywords: lambda-calculus, simple types, intersection types, strong normalization, mechanization, perpetual reductions}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.28
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.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
DOI: 10.4230/LIPIcs.CONCUR.2023.32
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.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
DOI: 10.4230/OASIcs.EVCS.2023.2
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.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
DOI: 10.4230/LIPIcs.CONCUR.2021.31
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.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
DOI: 10.4230/LIPIcs.CONCUR.2020.8
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.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
DOI: 10.4230/LIPIcs.FSCD.2020.20
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.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
DOI: 10.4230/DagSemProc.06351.12
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.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 Dudenhefner, Andrej
  • 1 Erkens, Rick
  • 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
  • 8 document

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

© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact