arXiv subjects

Sławomir Lasota

Publications and source records attributed to Sławomir Lasota.

At least 37 records · Page 2Linked to original sources

arXiv2020

VASS reachability in three steps

This note is a product of digestion of the famous proof of decidability of the reachability problem for vector addition systems with states (VASS), as first established by Mayr in 1981 and then simplified by Kosaraju in 1982. The note is neither intended to be rigorously formal nor complete; it is rather intended to be an intuitive but precise enough description of main concepts exploited in the proof. Very roughly, the overall idea is to provide a decidable condition Theta on a VASS such that Theta implies reachability and its negation implies that the size of VASS can be reduced. With these two properties, the size of input can be incrementally reduced until the problem becomes trivial. We proceed in three steps: we first formulate the condition Theta for plain VASS, then adapt it to more general VASS with unconstrained coordinates, and finally to generalized VASS of Kosaraju.

cs.LO↗

arXiv2020

Reachability in fixed dimension vector addition systems with states

The reachability problem is a central decision problem for formal verification based on vector addition systems with states (VASS), which are equivalent to Petri nets and form one of the most studied and applied models of concurrency. Reachability for VASS is also inter-reducible with a plethora of problems from a number of areas of computer science. In spite of recent progress, the complexity of the reachability problem remains unsettled, and it is closely related to the lengths of shortest VASS runs that witness reachability. We consider VASS of fixed dimension, and obtain three main results. For the first two, we assume that the integers in the input are given in unary, and that the control graph of the given VASS is flat (i.e., without nested cycles). We obtain a family of VASS in dimension 3 whose shortest reachability witnessing runs are exponential, and we show that the reachability problem is NP-hard in dimension 7. These results resolve negatively questions that had been posed by the works of Blondin et al. in LICS 2015 and Englert et al. in LICS 2016, and contribute a first construction that distinguishes 3-dimensional flat VASS from 2-dimensional VASS. Our third result, by means of a novel family of products of integer fractions, shows that 4-dimensional VASS can have doubly exponentially long shortest reachability witnessing runs. The smallest dimension for which this was previously known is 14.

cs.FL↗

arXiv2020

Timed games and deterministic separability

We study a generalisation of Büchi-Landweber games to the timed setting. The winning condition is specified by a non-deterministic timed automaton with epsilon transitions and only Player I can elapse time. We show that for fixed number of clocks and maximal numerical constant available to Player II, it is decidable whether she has a winning timed controller using these resources. More interestingly, we also show that the problem remains decidable even when the maximal numerical constant is not specified in advance, which is an important technical novelty not present in previous literature on timed games. We complement these two decidability result by showing undecidability when the number of clocks available to Player II is not fixed. As an application of timed games, and our main motivation to study them, we show that they can be used to solve the deterministic separability problem for nondeterministic timed automata with epsilon transitions. This is a novel decision problem about timed automata which has not been studied before. We show that separability is decidable when the number of clocks of the separating automaton is fixed and the maximal constant is not. The problem whether separability is decidable without bounding the number of clocks of the separator remains an interesting open problem.

cs.FL↗

arXiv2020

WQO dichotomy for 3-graphs

We investigate data-enriched models, like Petri nets with data, where executability of a transition is conditioned by a relation between data values involved. Decidability status of various decision problems in such models may depend on the structure of data domain. According to the WQO Dichotomy Conjecture, if a data domain is homogeneous then it either exhibits a well quasi-order (in which case decidability follows by standard arguments), or essentially all the decision problems are undecidable for Petri nets over that data domain. We confirm the conjecture for data domains being 3-graphs (graphs with 2-colored edges). On the technical level, this results is a significant step beyond known classification results for homogeneous structures.

cs.LO↗

arXiv2019

Definable isomorphism problem

We investigate the isomorphism problem in the setting of definable sets (equivalent to sets with atoms): given two definable relational structures, are they related by a definable isomorphism? Under mild assumptions on the underlying structure of atoms, we prove decidability of the problem. The core result is parameter-elimination: existence of an isomorphism definable with parameters implies existence of an isomorphism definable without parameters.

cs.LO↗

arXiv2019

New Pumping Technique for 2-dimensional VASS

We propose a new pumping technique for 2-dimensional vector addition systems with states (2-VASS) building on natural geometric properties of runs. We illustrate its applicability by reproving an exponential bound on the length of the shortest accepting run, and by proving a new pumping lemma for languages of 2-VASS. The technique is expected to be useful for settling questions concerning languages of 2-VASS, e.g., for establishing decidability status of the regular separability problem.

cs.FL↗

arXiv2019

Regular Separability of One Counter Automata

The regular separability problem asks, for two given languages, if there exists a regular language including one of them but disjoint from the other. Our main result is decidability, and PSpace-completeness, of the regular separability problem for languages of one counter automata without zero tests (also known as one counter nets). This contrasts with undecidability of the regularity problem for one counter nets, and with undecidability of the regular separability problem for one counter automata, which is our second result.

cs.FL↗

arXiv2018

Regular Separability of Well Structured Transition Systems

We investigate the languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility. Our first result shows that, under very mild assumptions, every two disjoint WSTS languages are regular separable: There is a regular language containing one of them and being disjoint from the other. As a consequence, if a language as well as its complement are both recognized by WSTS, then they are necessarily regular. In particular, no subclass of WSTS languages beyond the regular languages is closed under complement. Our second result shows that for Petri nets, the complexity of the backwards coverability algorithm yields a bound on the size of the regular separator. We complement it by a lower bound construction.

cs.FL↗

arXiv2018

Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms

We study an expressive model of timed pushdown automata extended with modular and fractional clock constraints. We show that the binary reachability relation is effectively expressible in hybrid linear arithmetic with a rational and an integer sort. This subsumes analogous expressibility results previously known for finite and pushdown timed automata with untimed stack. As key technical tools, we use quantifier elimination for a fragment of hybrid linear arithmetic and for cyclic order atoms, and a reduction to register pushdown automata over cyclic order atoms.

cs.FL↗

arXiv2018

Linear Equations with Ordered Data

Following a recently considered generalization of linear equations to unordered data vectors, we perform a further generalization to ordered data vectors. These generalized equations naturally appear in the analysis of vector addition systems (or Petri nets) extended with ordered data. We show that nonnegative-integer solvability of linear equations is computationally equivalent (up to an exponential blowup) with the reachability problem for (plain) vector addition systems. This high complexity is surprising, and contrasts with NP-completeness for unordered data vectors. Also surprisingly, we achieve polynomial time complexity of the solvability problem when the nonnegative-integer restriction on solutions is dropped.

cs.LO↗

arXiv2016

Regular Separability of Parikh Automata

We investigate a subclass of languages recognized by vector addition systems, namely languages of nondeterministic Parikh automata. While the regularity problem (is the language of a given automaton regular?) is undecidable for this model, we show surprising decidability of the regular separability problem: given two Parikh automata, is there a regular language that contains one of them and is disjoint from the other?

cs.FL↗

arXiv2016

Separability of Reachability Sets of Vector Addition Systems

Given two families of sets $\mathcal{F}$ and $\mathcal{G}$, the $\mathcal{F}$ separability problem for $\mathcal{G}$ asks whether for two given sets $U, V \in \mathcal{G}$ there exists a set $S \in \mathcal{F}$, such that $U$ is included in $S$ and $V$ is disjoint with $S$. We consider two families of sets $\mathcal{F}$: modular sets $S \subseteq \mathbb{N}^d$, defined as unions of equivalence classes modulo some natural number $n \in \mathbb{N}$, and unary sets. Our main result is decidability of modular and unary separability for the class $\mathcal{G}$ of reachability sets of Vector Addition Systems, Petri Nets, Vector Addition Systems with States, and for sections thereof.

cs.FL↗

arXiv2016

Equivariant algorithms for constraint satisfaction problems over coset templates

We investigate the Constraint Satisfaction Problem (CSP) over templates with a group structure, and algorithms solving CSP that are equivariant, i.e. invariant under a natural group action induced by a template. Our main result is a method of proving the implication: if CSP over a coset template T is solvable by an equivariant algorithm then T is 2-Helly (or equivalently, has a majority polymorphism). Therefore bounded width, and definability in fixed-point logics, coincide with 2-Helly. Even if these facts may be derived from already known results, our new proof method has two advantages. First, the proof is short, self-contained, and completely avoids referring to the omitting-types theorems. Second, it brings to light some new connections between CSP theory and descriptive complexity theory, via a construction similar to CFI graphs.

cs.LO↗

arXiv2015

Reachability analysis of first-order definable pushdown systems

We study pushdown systems where control states, stack alphabet, and transition relation, instead of being finite, are first-order definable in a fixed countably-infinite structure. We show that the reachability analysis can be addressed with the well-known saturation technique for the wide class of oligomorphic structures. Moreover, for the more restrictive homogeneous structures, we are able to give concrete complexity upper bounds. We show ample applicability of our technique by presenting several concrete examples of homogeneous structures, subsuming, with optimal complexity, known results from the literature. We show that infinitely many such examples of homogeneous structures can be obtained with the classical wreath product construction.

cs.FL↗

arXiv2015

Timed pushdown automata revisited

This paper contains two results on timed extensions of pushdown automata (PDA). As our first result we prove that the model of dense-timed PDA of Abdulla et al. collapses: it is expressively equivalent to dense-timed PDA with timeless stack. Motivated by this result, we advocate the framework of first-order definable PDA, a specialization of PDA in sets with atoms, as the right setting to define and investigate timed extensions of PDA. The general model obtained in this way is Turing complete. As our second result we prove NEXPTIME upper complexity bound for the non-emptiness problem for an expressive subclass. As a byproduct, we obtain a tight EXPTIME complexity bound for a more restrictive subclass of PDA with timeless stack, thus subsuming the complexity bound known for dense-timed PDA.

cs.FL↗

arXiv2014

Automata theory in nominal sets

We study languages over infinite alphabets equipped with some structure that can be tested by recognizing automata. We develop a framework for studying such alphabets and the ensuing automata theory, where the key role is played by an automorphism group of the alphabet. In the process, we generalize nominal sets due to Gabbay and Pitts.

cs.LO↗

arXiv2013

Modelling the efficacy of hyperthermia treatment

Multimodal oncological strategies which combine chemotherapy or radiotherapy with hyperthermia have a potential of improving the efficacy of the non-surgical methods of cancer treatment. Hyperthermia engages the heat-shock response mechanism (HSR), main component of which are heat-shock proteins (HSP). Cancer cells have already partially activated HSR, thereby, hyperthermia may be more toxic to them relative to normal cells. On the other hand, HSR triggers thermotolerance, i.e. hyperthermia treated cells show an impairment in their susceptibility to a subsequent heat-induced stress. This poses questions about efficacy and optimal strategy of the anti-cancer therapy combined with hyperthermia treatment. To address these questions, we adapt our previous HSR model and propose its stochastic extension. We formalise the notion of a HSP-induced thermotolerance. Next, we estimate the intensity and the duration of the thermotolerance. Finally, we quantify the effect of a multimodal therapy based on hyperthermia and a cytotoxic effect of bortezomib, a clinically approved proteasome inhibitor. Consequently, we propose an optimal strategy for combining hyperthermia and proteasome inhibition modalities. In summary, by a proof of concept mathematical analysis of HSR we are able to support the common belief that the combination of cancer treatment strategies increases therapy efficacy. thermotolerance.

q-bio.SC↗

arXiv2012

Minimization of semilinear automata

We investigate finite deterministic automata in sets with non-homogeneous atoms: integers with successor. As there are uncount- ably many deterministic finite automata in this setting, we restrict our attention to automata with semilinear transition function. The main re- sults is a minimization procedure for semilinear automata. The proof is subtle and refers to decidability of existential Presburger arithmetic with divisibility predicates. Interestingly, the minimization is not obtained by the standard partition refinement procedure, and we demonstrate that this procedure does not necessarily terminate for semilinear automata.

cs.LO↗