Search Results

Documents authored by Tzevelekos, Nikos

Document
DOI: 10.4230/LIPIcs.MFCS.2025.14
Register Automata with Permutations

Authors: Mrudula Balachander, Emmanuel Filiot, Raffaella Gentilini, and Nikos Tzevelekos

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
We propose Permutation Deterministic Register Automata (pDRAs), a deterministic register automaton model where we allow permutations of registers in transitions. The model enables minimal canonical representations and pDRAs can be tested for equivalence in polynomial time. The complexity of minimization is between GI (the complexity of graph isomorphism) and NP. We then introduce a subclass of pDRAs, called register automata with fixed permutation policy, where the register permutation discipline is stipulated globally. This class generalizes the model proposed by Benedikt, Ley and Puppis in 2010, and we show that it also admits minimal and canonical representations, based on a finite-index word equivalence relation. As an application, we show that for any regular data language L, the minimal register automaton with fixed permutation policy recognizing L can be actively learned in polynomial time using oracles for membership, equivalence and data-memorability queries. We show that all the oracles can be implemented in polynomial time, and so this yields a polynomial time minimization algorithm.
Cite as

Mrudula Balachander, Emmanuel Filiot, Raffaella Gentilini, and Nikos Tzevelekos. Register Automata with Permutations. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{balachander_et_al:LIPIcs.MFCS.2025.14,
  author =	{Balachander, Mrudula and Filiot, Emmanuel and Gentilini, Raffaella and Tzevelekos, Nikos},
  title =	{{Register Automata with Permutations}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.14},
  URN =		{urn:nbn:de:0030-drops-241219},
  doi =		{10.4230/LIPIcs.MFCS.2025.14},
  annote =	{Keywords: Register automata, data words, equivalence, minimization, active learning}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.27
Symbolic Execution Game Semantics

Authors: Yu-Yang Lin and Nikos Tzevelekos

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

Abstract
We present a framework for symbolically executing and model checking higher-order programs with external (open) methods. We focus on the client-library paradigm and in particular we aim to check libraries with respect to any definable client. We combine traditional symbolic execution techniques with operational game semantics to build a symbolic execution semantics that captures arbitrary external behaviour. We prove the symbolic semantics to be sound and complete. This yields a bounded technique by imposing bounds on the depth of recursion and callbacks. We provide an implementation of our technique in the 𝕂 framework and showcase its performance on a custom benchmark based on higher-order coding errors such as reentrancy bugs.
Cite as

Yu-Yang Lin and Nikos Tzevelekos. Symbolic Execution Game Semantics. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 27:1-27:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{lin_et_al:LIPIcs.FSCD.2020.27,
  author =	{Lin, Yu-Yang and Tzevelekos, Nikos},
  title =	{{Symbolic Execution Game Semantics}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{27:1--27:24},
  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.27},
  URN =		{urn:nbn:de:0030-drops-123493},
  doi =		{10.4230/LIPIcs.FSCD.2020.27},
  annote =	{Keywords: game semantics, symbolic execution, higher-order open programs}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2018.72
Polynomial-Time Equivalence Testing for Deterministic Fresh-Register Automata

Authors: Andrzej S. Murawski, Steven J. Ramsay, and Nikos Tzevelekos

Published in: LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)

Abstract
Register automata are one of the most studied automata models over infinite alphabets. The complexity of language equivalence for register automata is quite subtle. In general, the problem is undecidable but, in the deterministic case, it is known to be decidable and in NP. Here we propose a polynomial-time algorithm building upon automata- and group-theoretic techniques. The algorithm is applicable to standard register automata with a fixed number of registers as well as their variants with a variable number of registers and ability to generate fresh data values (fresh-register automata). To complement our findings, we also investigate the associated inclusion problem and show that it is PSPACE-complete.
Cite as

Andrzej S. Murawski, Steven J. Ramsay, and Nikos Tzevelekos. Polynomial-Time Equivalence Testing for Deterministic Fresh-Register Automata. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 72:1-72:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{murawski_et_al:LIPIcs.MFCS.2018.72,
  author =	{Murawski, Andrzej S. and Ramsay, Steven J. and Tzevelekos, Nikos},
  title =	{{Polynomial-Time Equivalence Testing for Deterministic Fresh-Register Automata}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{72:1--72:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Potapov, Igor and Spirakis, Paul and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2018.72},
  URN =		{urn:nbn:de:0030-drops-96544},
  doi =		{10.4230/LIPIcs.MFCS.2018.72},
  annote =	{Keywords: automata over infinite alphabets, language equivalence, bisimilarity, computational group theory}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.34
Higher-Order Linearisability

Authors: Andrzej S. Murawski and Nikos Tzevelekos

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
Linearisability is a central notion for verifying concurrent libraries: a library is proven correct if its operational history can be rearranged into a sequential one that satisfies a given specification. Until now, linearisability has been examined for libraries in which method arguments and method results were of ground type. In this paper we extend linearisability to the general higher-order setting, where methods of arbitrary type can be passed as arguments and returned as values, and establish its soundness.
Cite as

Andrzej S. Murawski and Nikos Tzevelekos. Higher-Order Linearisability. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 34:1-34:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{murawski_et_al:LIPIcs.CONCUR.2017.34,
  author =	{Murawski, Andrzej S. and Tzevelekos, Nikos},
  title =	{{Higher-Order Linearisability}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{34:1--34:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.34},
  URN =		{urn:nbn:de:0030-drops-78035},
  doi =		{10.4230/LIPIcs.CONCUR.2017.34},
  annote =	{Keywords: Linearisability, Concurrency, Higher-Order Computation}
}
Document
DOI: 10.4230/DagSemProc.10351.5
Program Equivalence with Names

Authors: Nikos Tzevelekos

Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)

Abstract
The nu-calculus of Pitts and Stark was introduced as a paradigmatic functional language with a very basic local-state effect: references of unit type. These were called names, and the motto of the new language went as follows: "Names are created with local scope, can be tested for equality, and are passed around via function application, but that is all." Because of this limited framework, the hope was that fully abstract models and complete proof techniques could be obtained. However, it was soon realised that the behaviour of nu-calculus programs is quite intricate, and program equivalence in particular is surprisingly difficult to capture. Here we shall focus on the following "hard" equivalence. new x,y in f. (fx=fy) == f. true We shall examine attempts and proofs of the above, explain the advantages and disadvantages of the proof methods and discuss why program equivalence in this simple language remains to date a mystery.
Cite as

Nikos Tzevelekos. Program Equivalence with Names. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{tzevelekos:DagSemProc.10351.5,
  author =	{Tzevelekos, Nikos},
  title =	{{Program Equivalence with Names}},
  booktitle =	{Modelling, Controlling and Reasoning About State},
  pages =	{1--18},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10351},
  editor =	{Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.5},
  URN =		{urn:nbn:de:0030-drops-28092},
  doi =		{10.4230/DagSemProc.10351.5},
  annote =	{Keywords: Nu-calculus, Local State, Logical Relations, Game Semantics, Environmental Bisimulations}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact