2 Search Results for "Koutavas, Vasileios"

Document
DOI: 10.4230/LIPIcs.CSL.2026.23
A Logic for Fresh Labelled Transition Systems

Authors: Mohamed H. Bandukara and Nikos Tzevelekos

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We introduce a Hennessy-Milner logic with recursion for Fresh Labelled Transition Systems (FLTSs). These are nominal labelled transition systems which keep track of the history, i.e. of data values seen so far, and can model fresh data generation. In particular, FLTSs generalise the computations of Fresh-Register Automata, which in turn can be seen as a "regular" class of history-tracking automata operating on infinite input alphabets. The logic we introduce is a modal mu-calculus equipped with infinite disjunctions over arbitrary and fresh data values respectively, while its recursion is parameterised on vectors of data values. It can express a variety of properties, such as the existence of an infinite path of distinct data values, the absence of paths where values are repeated, or the existence of a finite path where some taint property is violated. We study the model-checking problem and its complexity via a reduction to parity games and, using nominal sets techniques, provide an exponential upper bound for it.
Cite as

Mohamed H. Bandukara and Nikos Tzevelekos. A Logic for Fresh Labelled Transition Systems. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 23:1-23:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bandukara_et_al:LIPIcs.CSL.2026.23,
  author =	{Bandukara, Mohamed H. and Tzevelekos, Nikos},
  title =	{{A Logic for Fresh Labelled Transition Systems}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{23:1--23:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.23},
  URN =		{urn:nbn:de:0030-drops-254478},
  doi =		{10.4230/LIPIcs.CSL.2026.23},
  annote =	{Keywords: Nominal Transition Systems, Hennessy-Milner Logic, Modal Mu-Calculus, Register Automata, Nominal Sets, Parity Games}
}
Document
DOI: 10.4230/DagSemProc.10351.4
Limitations of Applicative Bisimulation (Preliminary Report)

Authors: Vasileios Koutavas, Paul Blain Levy, and Eijiro Sumii

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

Abstract
We present a series of examples that illuminate an important aspect of the semantics of higher-order functions with local state. Namely that certain behaviour of such functions can only be observed by pro- viding them with arguments that contain the functions themselves. This provides evidence for the necessity of complex conditions for functions in modern semantics for state, such as logical relations and Kripke-like bisimulations, where related functions are applied to related arguments (that may contain the functions). It also suggests that simpler semantics, such as those based on applicative bisimulations where functions are ap- plied to identical arguments, would not scale to higher-order languages with local state.
Cite as

Vasileios Koutavas, Paul Blain Levy, and Eijiro Sumii. Limitations of Applicative Bisimulation (Preliminary Report). In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{koutavas_et_al:DagSemProc.10351.4,
  author =	{Koutavas, Vasileios and Levy, Paul Blain and Sumii, Eijiro},
  title =	{{Limitations of Applicative Bisimulation (Preliminary Report)}},
  booktitle =	{Modelling, Controlling and Reasoning About State},
  pages =	{1--9},
  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.4},
  URN =		{urn:nbn:de:0030-drops-28074},
  doi =		{10.4230/DagSemProc.10351.4},
  annote =	{Keywords: Imperative languages, higher-order functions, local state}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 1 2010

  • Refine by Author
  • 1 Bandukara, Mohamed H.
  • 1 Koutavas, Vasileios
  • 1 Levy, Paul Blain
  • 1 Sumii, Eijiro
  • 1 Tzevelekos, Nikos

  • Refine by Series/Journal
  • 1 LIPIcs
  • 1 DagSemProc

  • Refine by Classification
  • 1 Theory of computation → Automata over infinite objects
  • 1 Theory of computation → Modal and temporal logics

  • Refine by Keyword
  • 1 Hennessy-Milner Logic
  • 1 Imperative languages
  • 1 Modal Mu-Calculus
  • 1 Nominal Sets
  • 1 Nominal Transition Systems
  • Show More...

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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact