Arrow Research search

Author name cluster

Patrick Totzke

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

11 papers
2 author rows

Possible papers

11

GandALF Workshop 2023 Workshop Paper

Handling of Past and Future with Phenesthe+

  • Manolis Pitsikalis
  • Alexei Lisitsa
  • Patrick Totzke

Writing temporal logic formulae for properties that combine instantaneous events with overlapping temporal phenomena of some duration is difficult in classical temporal logics. To address this issue, in previous work we introduced a new temporal logic with intuitive temporal modalities specifically tailored for the representation of both instantaneous and durative phenomena. We also provided an implementation of a complex event processing system, Phenesthe, based on this logic, that has been applied and tested on a real maritime surveillance scenario. In this work, we extend our temporal logic with two extra modalities to increase its expressive power for handling future formulae. We compare the expressive power of different fragments of our logic with Linear Temporal Logic and dyadic first-order logic. Furthermore, we define correctness criteria for stream processors that use our language. Last but not least, we evaluate empirically the performance of Phenesthe+, our extended implementation, and show that the increased expressive power does not affect efficiency significantly.

PDF Details DOI

MFCS Conference 2021 Conference Paper

HyperLTL Satisfiability Is Σ₁¹-Complete, HyperCTL* Satisfiability Is Σ₁²-Complete

  • Marie Fortin
  • Louwe B. Kuijer
  • Patrick Totzke
  • Martin Zimmermann 0002

Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. The two most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by trace quantification. It is known that this expressiveness comes at a price, i. e. satisfiability is undecidable for both logics. In this paper we settle the exact complexity of these problems, showing that both are in fact highly undecidable: we prove that HyperLTL satisfiability is Σ₁¹-complete and HyperCTL* satisfiability is Σ₁²-complete. These are significant increases over the previously known lower bounds and the first upper bounds. To prove Σ₁²-membership for HyperCTL*, we prove that every satisfiable HyperCTL* sentence has a model that is equinumerous to the continuum, the first upper bound of this kind. We prove this bound to be tight. Finally, we show that the membership problem for every level of the HyperLTL quantifier alternation hierarchy is Π₁¹-complete.

Details

MFCS Conference 2020 Conference Paper

Optimally Resilient Strategies in Pushdown Safety Games

  • Daniel Neider
  • Patrick Totzke
  • Martin Zimmermann 0002

Infinite-duration games with disturbances extend the classical framework of infinite-duration games, which captures the reactive synthesis problem, with a discrete measure of resilience against non-antagonistic external influence. This concerns events where the observed system behavior differs from the intended one prescribed by the controller. For games played on finite arenas it is known that computing optimally resilient strategies only incurs a polynomial overhead over solving classical games. This paper studies safety games with disturbances played on infinite arenas induced by pushdown systems. We show how to compute optimally resilient strategies in triply-exponential time. For the subclass of safety games played on one-counter configuration graphs, we show that determining the degree of resilience of the initial configuration is PSPACE-complete and that optimally resilient strategies can be computed in doubly-exponential time.

Details

Highlights Conference 2020 Conference Abstract

Parametrized Universality Problems for One-Counter Nets

  • Patrick Totzke

We study the language universality problem for One-Counter Nets, also known as 1-dimensional Vector Addition Systems with States (1-VASS), parameterized either with an initial counter value, or with an upper bound on the allowed counter value during runs. The language accepted by an OCN (defined by reaching a final control state) is monotone in both parameters. This yields two natural decision problems: 1. does there exist an initial counter value that makes the language universal? 2. does there exist a sufficiently high ceiling so that the bounded language is universal? Although the ordinary universality problem is decidable (and Ackermann-complete) and these parameterized variants seem to reduce to checking basic structural properties of the underlying automaton, we show that in fact both problems are undecidable. We also look into the complexities of the problems for several decidable subclasses, namely for unambiguous, and deterministic systems, and for those over a single-letter alphabet. This is joint work with Shaull Almagor, Udi Boker, and Piotr Hofman. The paper will be presented at CONCUR’20 and a full version is available on the arXiv: https: //arxiv. org/abs/2005. 03435.

PDF Details

Highlights Conference 2018 Conference Abstract

Universal Safety for Timed Petri Nets is PSPACE-complete

  • Patrick Totzke

ABSTRACT. Timed-arc Petri nets (TPN) are an extension of Petri nets where each token carries one real-valued clock and transitions are guarded by integer inequality constraints on clocks. We consider the model in which newly created tokens can either be reset, or inherit values of input tokens of the transition. The Existential Coverability problem for TPN asks, for a given place p and transition t, whether there exists a number m such that the marking M (m) = m·{(p, 0)} ultimately enables t. Here, M (m) contains exactly m tokens on place p with all clocks set to zero and no other tokens. This problem corresponds to checking safety properties in distributed networks of arbitrarily many (namely m) initially identical timed processes that communicate by handshake. A negative answer certifies that the ‘bad event’ of transition t can never happen regardless of the number m of processes, i. e. , the network is safe for any size. Thus by checking existential coverability, one solves the dual problem of Universal Safety. We show that both problems are decidable and PSPACE-complete. The lower bound is shown by a reduction from the iterated monotone Boolean circuit problem. The upper bound is shown by an acceleration technique for a suitable notion of (infinite) region automata. This moreover leads to a symbolic representation of the set of coverable configurations, which can be computed in exponential space.

Details

Highlights Conference 2016 Conference Abstract

Reachability in two-dimensional unary vector addition systems with states is NL-complete

  • Matthias Englert
  • Ranko Lazic
  • Patrick Totzke

Blondin et al. showed at LICS 2015 that two-dimensional vector addition systems with states have reachability witnesses of length exponential in the number of states and polynomial in the norm of vectors. The resulting guess-and-verify algorithm is optimal (PSPACE), but only if the input vectors are given in binary. We answer positively the main question left open by their work, namely establish that reachability witnesses of pseudo-polynomial length always exist. Hence, when the input vectors are given in unary, the improved guess-and-verify algorithm requires only logarithmic space. Joint work with Matthias Englert and Patrick Totzke, to appear in LICS 2016. Available from: http: //arxiv. org/abs/1602. 00477

Details

Highlights Conference 2015 Conference Abstract

Contex-Free Controlled Vector Addition Systems

  • Patrick Totzke

I propose to present recent and ongoing work on Pushdown VASS, that ex- tend Vector Addition Systems with a stack. What can be modelled with these systems? What are interesting open problems and how to attack them? In [4] we discussed an equivalent formalism, which amounts to VASS that allow only runs from a context-free control language, similar to the regulated rewriting setting [1]. Reachability problems like coverability and boundedness can then be attacked by analysing annotated derivation trees of a GfG. This not only helps to simplify proofs but also to address slightly more general problems. This is joint work with Jerome Leroux and Gregoire Sutre.

Details

Highlights Conference 2013 Conference Abstract

Decidability of weak simulation on one-counter nets

  • Piotr Hofman
  • Richard Mayr
  • Patrick Totzke

One-counter nets (OCN) are Petri nets with exactly one unbounded place. They are equivalent to a subclass of one-counter automata with only a weak test for zero. We show that weak simulation preorder is decidable for OCN. In contrast, other semantic relations like weak bisimulation are undecidable for OCN, and so are weak (and strong) trace inclusion.

PDF Details