-
An Axiomatic Assessment of Entropy- and Variance-based Uncertainty Quantification in Regression
Authors:
Christopher Bülte,
Yusuf Sale,
Timo Löhr,
Paul Hofman,
Gitta Kutyniok,
Eyke Hüllermeier
Abstract:
Uncertainty quantification (UQ) is crucial in machine learning, yet most (axiomatic) studies of uncertainty measures focus on classification, leaving a gap in regression settings with limited formal justification and evaluations. In this work, we introduce a set of axioms to rigorously assess measures of aleatoric, epistemic, and total uncertainty in supervised regression. By utilizing a predictiv…
▽ More
Uncertainty quantification (UQ) is crucial in machine learning, yet most (axiomatic) studies of uncertainty measures focus on classification, leaving a gap in regression settings with limited formal justification and evaluations. In this work, we introduce a set of axioms to rigorously assess measures of aleatoric, epistemic, and total uncertainty in supervised regression. By utilizing a predictive exponential family, we can generalize commonly used approaches for uncertainty representation and corresponding uncertainty measures. More specifically, we analyze the widely used entropy- and variance-based measures regarding limitations and challenges. Our findings provide a principled foundation for uncertainty quantification in regression, offering theoretical insights and practical guidelines for reliable uncertainty assessment.
△ Less
Submitted 16 May, 2025; v1 submitted 25 April, 2025;
originally announced April 2025.
-
A viscoplasticity model with an invariant-based non-Newtonian flow rule for unidirectional thermoplastic composites
Authors:
P. Hofman,
D. Kovačević,
F. P. van der Meer,
L. J. Sluys
Abstract:
A three-dimensional mesoscopic viscoplasticity model for simulating rate-dependent plasticity and creep in unidirectional thermoplastic composites is presented. The constitutive model is a transversely isotropic extension of an isotropic finite strain viscoplasticity model for neat polymers. Rate-dependent plasticity and creep are described by a non-Newtonian flow rule where the viscosity of the m…
▽ More
A three-dimensional mesoscopic viscoplasticity model for simulating rate-dependent plasticity and creep in unidirectional thermoplastic composites is presented. The constitutive model is a transversely isotropic extension of an isotropic finite strain viscoplasticity model for neat polymers. Rate-dependent plasticity and creep are described by a non-Newtonian flow rule where the viscosity of the material depends on an equivalent stress measure through an Eyring-type relation. In the present formulation, transverse isotropy is incorporated by defining the equivalent stress measure and flow rule as functions of transversely isotropic stress invariants. In addition, the Eyring-type viscosity function is extended with anisotropic pressure dependence. As a result of the formulation, plastic flow in fiber direction is effectively excluded and pressure dependence of the polymer matrix is accounted for. The re-orientation of the transversely isotropic plane during plastic deformations is incorporated in the constitutive equations, allowing for an accurate large deformation response. The formulation is fully implicit and a consistent linearization of the algorithmic constitutive equations is performed to derive the consistent tangent modulus. The performance of the mesoscopic constitutive model is assessed through a comparison with a micromechanical model for carbon/PEEK, with the original isotropic viscoplastic version for the polymer matrix and with hyperelastic fibers. The micromodel is first used to determine the material parameters of the mesoscale model with a few stress-strain curves. It is demonstrated that the mesoscale model gives a similar response to the micromodel under various loading conditions. Finally, the mesoscale model is validated against off-axis experiments on unidirectional thermoplastic composite plies.
△ Less
Submitted 16 April, 2025;
originally announced April 2025.
-
Soundness of reset workflow nets
Authors:
Michael Blondin,
Alain Finkel,
Piotr Hofman,
Filip Mazowiecki,
Philip Offtermatt
Abstract:
Workflow nets are a well-established variant of Petri nets for the modeling of process activities such as business processes. The standard correctness notion of workflow nets is soundness, which comes in several variants. Their decidability was shown decades ago, but their complexity was only identified recently. In this work, we are primarily interested in two popular variants: $1$-soundness and…
▽ More
Workflow nets are a well-established variant of Petri nets for the modeling of process activities such as business processes. The standard correctness notion of workflow nets is soundness, which comes in several variants. Their decidability was shown decades ago, but their complexity was only identified recently. In this work, we are primarily interested in two popular variants: $1$-soundness and generalised soundness.
Workflow nets have been extended with resets to model workflows that can, e.g., cancel actions. It has been known for a while that, for this extension, all variants of soundness, except possibly generalised soundness, are undecidable.
We complete the picture by showing that generalised soundness is also undecidable for reset workflow nets. We then blur this undecidability landscape by identifying a property, coined ``$1$-in-between soundness'', which lies between $1$-soundness and generalised soundness. It reveals an unusual non-monotonic complexity behaviour: a decidable soundness property is in between two undecidable ones. This can be valuable in the algorithmic analysis of reset workflow nets, as our procedure yields an output of the form ``$1$-sound'' or ``not generalised sound'' which is always correct.
△ Less
Submitted 6 March, 2025;
originally announced March 2025.
-
Label-wise Aleatoric and Epistemic Uncertainty Quantification
Authors:
Yusuf Sale,
Paul Hofman,
Timo Löhr,
Lisa Wimmer,
Thomas Nagler,
Eyke Hüllermeier
Abstract:
We present a novel approach to uncertainty quantification in classification tasks based on label-wise decomposition of uncertainty measures. This label-wise perspective allows uncertainty to be quantified at the individual class level, thereby improving cost-sensitive decision-making and helping understand the sources of uncertainty. Furthermore, it allows to define total, aleatoric, and epistemic…
▽ More
We present a novel approach to uncertainty quantification in classification tasks based on label-wise decomposition of uncertainty measures. This label-wise perspective allows uncertainty to be quantified at the individual class level, thereby improving cost-sensitive decision-making and helping understand the sources of uncertainty. Furthermore, it allows to define total, aleatoric, and epistemic uncertainty on the basis of non-categorical measures such as variance, going beyond common entropy-based measures. In particular, variance-based measures address some of the limitations associated with established methods that have recently been discussed in the literature. We show that our proposed measures adhere to a number of desirable properties. Through empirical evaluation on a variety of benchmark data sets -- including applications in the medical domain where accurate uncertainty quantification is crucial -- we establish the effectiveness of label-wise uncertainty quantification.
△ Less
Submitted 4 June, 2024;
originally announced June 2024.
-
Quantifying Aleatoric and Epistemic Uncertainty with Proper Scoring Rules
Authors:
Paul Hofman,
Yusuf Sale,
Eyke Hüllermeier
Abstract:
Uncertainty representation and quantification are paramount in machine learning and constitute an important prerequisite for safety-critical applications. In this paper, we propose novel measures for the quantification of aleatoric and epistemic uncertainty based on proper scoring rules, which are loss functions with the meaningful property that they incentivize the learner to predict ground-truth…
▽ More
Uncertainty representation and quantification are paramount in machine learning and constitute an important prerequisite for safety-critical applications. In this paper, we propose novel measures for the quantification of aleatoric and epistemic uncertainty based on proper scoring rules, which are loss functions with the meaningful property that they incentivize the learner to predict ground-truth (conditional) probabilities. We assume two common representations of (epistemic) uncertainty, namely, in terms of a credal set, i.e. a set of probability distributions, or a second-order distribution, i.e., a distribution over probability distributions. Our framework establishes a natural bridge between these representations. We provide a formal justification of our approach and introduce new measures of epistemic and aleatoric uncertainty as concrete instantiations.
△ Less
Submitted 19 April, 2024; v1 submitted 18 April, 2024;
originally announced April 2024.
-
Modeling of progressive high-cycle fatigue in composite laminates accounting for local stress ratios
Authors:
P. Hofman,
F. P. van der Meer,
L. J. Sluys
Abstract:
A numerical framework for simulating progressive failure under high-cycle fatigue loading is validated against experiments of composite quasi-isotropic open-hole laminates. Transverse matrix cracking and delamination are modeled with a mixed-mode fatigue cohesive zone model, covering crack initiation and propagation. Furthermore, XFEM is used for simulating transverse matrix cracks and splits at a…
▽ More
A numerical framework for simulating progressive failure under high-cycle fatigue loading is validated against experiments of composite quasi-isotropic open-hole laminates. Transverse matrix cracking and delamination are modeled with a mixed-mode fatigue cohesive zone model, covering crack initiation and propagation. Furthermore, XFEM is used for simulating transverse matrix cracks and splits at arbitrary locations. An adaptive cycle jump approach is employed for efficiently simulating high-cycle fatigue while accounting for local stress ratio variations in the presence of thermal residual stresses. The cycle jump scheme is integrated in the XFEM framework, where the local stress ratio is used to determine the insertion of cracks and to propagate fatigue damage. The fatigue cohesive zone model is based on S-N curves and requires static material properties and only a few fatigue parameters, calibrated on simple fracture testing specimens. The simulations demonstrate a good correspondence with experiments in terms of fatigue life and damage evolution.
△ Less
Submitted 8 March, 2024;
originally announced March 2024.
-
Second-Order Uncertainty Quantification: Variance-Based Measures
Authors:
Yusuf Sale,
Paul Hofman,
Lisa Wimmer,
Eyke Hüllermeier,
Thomas Nagler
Abstract:
Uncertainty quantification is a critical aspect of machine learning models, providing important insights into the reliability of predictions and aiding the decision-making process in real-world applications. This paper proposes a novel way to use variance-based measures to quantify uncertainty on the basis of second-order distributions in classification problems. A distinctive feature of the measu…
▽ More
Uncertainty quantification is a critical aspect of machine learning models, providing important insights into the reliability of predictions and aiding the decision-making process in real-world applications. This paper proposes a novel way to use variance-based measures to quantify uncertainty on the basis of second-order distributions in classification problems. A distinctive feature of the measures is the ability to reason about uncertainties on a class-based level, which is useful in situations where nuanced decision-making is required. Recalling some properties from the literature, we highlight that the variance-based measures satisfy important (axiomatic) properties. In addition to this axiomatic approach, we present empirical results showing the measures to be effective and competitive to commonly used entropy-based measures.
△ Less
Submitted 30 December, 2023;
originally announced January 2024.
-
Acyclic Petri and Workflow Nets with Resets
Authors:
Dmitry Chistikov,
Wojciech Czerwiński,
Piotr Hofman,
Filip Mazowiecki,
Henry Sinclair-Banks
Abstract:
In this paper we propose two new subclasses of Petri nets with resets, for which the reachability and coverability problems become tractable. Namely, we add an acyclicity condition that only applies to the consumptions and productions, not the resets. The first class is acyclic Petri nets with resets, and we show that coverability is PSPACE-complete for them. This contrasts the known Ackermann-har…
▽ More
In this paper we propose two new subclasses of Petri nets with resets, for which the reachability and coverability problems become tractable. Namely, we add an acyclicity condition that only applies to the consumptions and productions, not the resets. The first class is acyclic Petri nets with resets, and we show that coverability is PSPACE-complete for them. This contrasts the known Ackermann-hardness for coverability in (not necessarily acyclic) Petri nets with resets. We prove that the reachability problem remains undecidable for acyclic Petri nets with resets. The second class concerns workflow nets, a practically motivated and natural subclass of Petri nets. Here, we show that both coverability and reachability in acyclic workflow nets with resets are PSPACE-complete. Without the acyclicity condition, reachability and coverability in workflow nets with resets are known to be equally hard as for Petri nets with resets, that being Ackermann-hard and undecidable, respectively.
△ Less
Submitted 6 November, 2023; v1 submitted 3 October, 2023;
originally announced October 2023.
-
A numerical framework for simulating progressive failure in composite laminates under high-cycle fatigue loading
Authors:
Pieter Hofman,
Frans Paul van der Meer,
Lambertus Johannes Sluys
Abstract:
In this work, a recently proposed high-cycle fatigue cohesive zone model, which covers crack initiation and propagation with limited input parameters, is embedded in a robust and efficient numerical framework for simulating progressive failure in composite laminates under fatigue loading. The fatigue cohesive zone model is enhanced with an implicit time integration scheme of the fatigue damage var…
▽ More
In this work, a recently proposed high-cycle fatigue cohesive zone model, which covers crack initiation and propagation with limited input parameters, is embedded in a robust and efficient numerical framework for simulating progressive failure in composite laminates under fatigue loading. The fatigue cohesive zone model is enhanced with an implicit time integration scheme of the fatigue damage variable which allows for larger cycle increments and more efficient analyses. The method is combined with an adaptive strategy for determining the cycle increment based on global convergence rates. Moreover, a consistent material tangent stiffness matrix has been derived by fully linearizing the underlying mixed-mode quasi-static model and the fatigue damage update. The enhanced fatigue cohesive zone model is used to describe matrix cracking and delamination in laminates. In order to allow for matrix cracks to initiate at arbitrary locations and to avoid complex and costly mesh generation, the phantom node version of the eXtended finite element method (XFEM) is employed. For the insertion of new crack segments, an XFEM fatigue crack insertion criterion is presented, which is consistent with the fatigue cohesive zone formulation. It is shown with numerical examples that the improved fatigue damage update enhances the accuracy, efficiency and robustness of the numerical simulations significantly. The numerical framework is applied to the simulation of progressive fatigue failure in an open-hole [$\pm$45]-laminate. It is demonstrated that the numerical model is capable of accurately and efficiently simulating the complete failure process from distributed damage to localized failure.
△ Less
Submitted 22 September, 2023;
originally announced September 2023.
-
Conformal Prediction with Partially Labeled Data
Authors:
Alireza Javanmardi,
Yusuf Sale,
Paul Hofman,
Eyke Hüllermeier
Abstract:
While the predictions produced by conformal prediction are set-valued, the data used for training and calibration is supposed to be precise. In the setting of superset learning or learning from partial labels, a variant of weakly supervised learning, it is exactly the other way around: training data is possibly imprecise (set-valued), but the model induced from this data yields precise predictions…
▽ More
While the predictions produced by conformal prediction are set-valued, the data used for training and calibration is supposed to be precise. In the setting of superset learning or learning from partial labels, a variant of weakly supervised learning, it is exactly the other way around: training data is possibly imprecise (set-valued), but the model induced from this data yields precise predictions. In this paper, we combine the two settings by making conformal prediction amenable to set-valued training data. We propose a generalization of the conformal prediction procedure that can be applied to set-valued training and calibration data. We prove the validity of the proposed method and present experimental studies in which it compares favorably to natural baselines.
△ Less
Submitted 1 June, 2023;
originally announced June 2023.
-
Orbit-finite linear programming
Authors:
Arka Ghosh,
Piotr Hofman,
Sławomir Lasota
Abstract:
An infinite set is orbit-finite if, up to permutations of the underlying structure of atoms, it has only finitely many elements. We study a generalisation of linear programming where constraints are expressed by an orbit-finite system of linear inequalities. As our principal contribution we provide a decision procedure for checking if such a system has a real solution, and for computing the minima…
▽ More
An infinite set is orbit-finite if, up to permutations of the underlying structure of atoms, it has only finitely many elements. We study a generalisation of linear programming where constraints are expressed by an orbit-finite system of linear inequalities. As our principal contribution we provide a decision procedure for checking if such a system has a real solution, and for computing the minimal/maximal value of a linear objective function over the solution set. We also show undecidability of these problems in case when only integer solutions are considered. Therefore orbit-finite linear programming is decidable, while orbit-finite integer linear programming is not.
△ Less
Submitted 13 November, 2024; v1 submitted 1 February, 2023;
originally announced February 2023.
-
Quantifying Aleatoric and Epistemic Uncertainty in Machine Learning: Are Conditional Entropy and Mutual Information Appropriate Measures?
Authors:
Lisa Wimmer,
Yusuf Sale,
Paul Hofman,
Bern Bischl,
Eyke Hüllermeier
Abstract:
The quantification of aleatoric and epistemic uncertainty in terms of conditional entropy and mutual information, respectively, has recently become quite common in machine learning. While the properties of these measures, which are rooted in information theory, seem appealing at first glance, we identify various incoherencies that call their appropriateness into question. In addition to the measur…
▽ More
The quantification of aleatoric and epistemic uncertainty in terms of conditional entropy and mutual information, respectively, has recently become quite common in machine learning. While the properties of these measures, which are rooted in information theory, seem appealing at first glance, we identify various incoherencies that call their appropriateness into question. In addition to the measures themselves, we critically discuss the idea of an additive decomposition of total uncertainty into its aleatoric and epistemic constituents. Experiments across different computer vision tasks support our theoretical findings and raise concerns about current practice in uncertainty quantification.
△ Less
Submitted 25 June, 2023; v1 submitted 7 September, 2022;
originally announced September 2022.
-
Language Inclusion for Boundedly-Ambiguous Vector Addition Systems is Decidable
Authors:
Wojciech Czerwiński,
Piotr Hofman
Abstract:
We consider the problems of language inclusion and language equivalence for Vector Addition Systems with States (VASS) with the acceptance condition defined by the set of accepting states (and more generally by some upward-closed conditions). In general, the problem of language equivalence is undecidable even for one-dimensional VASS, thus to get decidability we investigate restricted subclasses.…
▽ More
We consider the problems of language inclusion and language equivalence for Vector Addition Systems with States (VASS) with the acceptance condition defined by the set of accepting states (and more generally by some upward-closed conditions). In general, the problem of language equivalence is undecidable even for one-dimensional VASS, thus to get decidability we investigate restricted subclasses. On the one hand, we show that the problem of language inclusion of a VASS in k-ambiguous VASS (for any natural k) is decidable and even in Ackermann. On the other hand, we prove that the language equivalence problem is already Ackermann-hard for deterministic VASS. These two results imply Ackermann-completeness for language inclusion and equivalence in several possible restrictions. Some of our techniques can be also applied in much broader generality in infinite-state systems, namely for some subclass of well-structured transition systems.
△ Less
Submitted 19 March, 2025; v1 submitted 16 February, 2022;
originally announced February 2022.
-
Solvability of orbit-finite systems of linear equations
Authors:
Arka Ghosh,
Piotr Hofman,
Sławomir Lasota
Abstract:
We study orbit-finite systems of linear equations, in the setting of sets with atoms. Our principal contribution is a decision procedure for solvability of such systems. The procedure works for every field (and even commutative ring) under mild effectiveness assumptions, and reduces a given orbit-finite system to a number of finite ones: exponentially many in general, but polynomially many when at…
▽ More
We study orbit-finite systems of linear equations, in the setting of sets with atoms. Our principal contribution is a decision procedure for solvability of such systems. The procedure works for every field (and even commutative ring) under mild effectiveness assumptions, and reduces a given orbit-finite system to a number of finite ones: exponentially many in general, but polynomially many when atom dimension of input systems is fixed. Towards obtaining the procedure we push further the theory of vector spaces generated by orbit-finite sets, and show that each such vector space admits an orbit-finite basis. This fundamental property is a key tool in our development, but should be also of wider interest.
△ Less
Submitted 10 June, 2022; v1 submitted 22 January, 2022;
originally announced January 2022.
-
Linear equations for unordered data vectors in $[D]^k\to{}Z^d$
Authors:
Piotr Hofman,
Jakub Różycki
Abstract:
Following a recently considered generalisation of linear equations to unordered-data vectors and to ordered-data vectors, we perform a further generalisation to data vectors that are functions from k-element subsets of the unordered-data set to vectors of integer numbers. These generalised equations naturally appear in the analysis of vector addition systems (or Petri nets) extended so that each t…
▽ More
Following a recently considered generalisation of linear equations to unordered-data vectors and to ordered-data vectors, we perform a further generalisation to data vectors that are functions from k-element subsets of the unordered-data set to vectors of integer numbers. These generalised equations naturally appear in the analysis of vector addition systems (or Petri nets) extended so that each token carries a set of unordered data. We show that nonnegative-integer solvability of linear equations is in nondeterministic exponential time while integer solvability is in polynomial time.
△ Less
Submitted 9 December, 2022; v1 submitted 9 August, 2021;
originally announced September 2021.
-
Parikh's theorem for infinite alphabets
Authors:
Piotr Hofman,
Marta Juzepczuk,
Sławomir Lasota,
Mohnish Pattathurajan
Abstract:
We investigate commutative images of languages recognised by register automata and grammars. Semi-linear and rational sets can be naturally extended to this setting by allowing for orbit-finite unions instead of only finite ones. We prove that commutative images of languages of one-register automata are not always semi-linear, but they are always rational. We also lift the latter result to grammar…
▽ More
We investigate commutative images of languages recognised by register automata and grammars. Semi-linear and rational sets can be naturally extended to this setting by allowing for orbit-finite unions instead of only finite ones. We prove that commutative images of languages of one-register automata are not always semi-linear, but they are always rational. We also lift the latter result to grammars: commutative images of one-register context-free languages are rational, and in consequence commutatively equivalent to register automata. We conjecture analogous results for automata and grammars with arbitrarily many registers.
△ Less
Submitted 24 April, 2021;
originally announced April 2021.
-
Universality Problem for Unambiguous VASS
Authors:
Wojciech Czerwiński,
Diego Figueira,
Piotr Hofman
Abstract:
We study languages of unambiguous VASS, that is, Vector Addition Systems with States, whose transitions read letters from a finite alphabet, and whose acceptance condition is defined by a set of final states (i.e., the coverability language). We show that the problem of universality for unambiguous VASS is ExpSpace-complete, in sheer contrast to Ackermann-completeness for arbitrary VASS, even in d…
▽ More
We study languages of unambiguous VASS, that is, Vector Addition Systems with States, whose transitions read letters from a finite alphabet, and whose acceptance condition is defined by a set of final states (i.e., the coverability language). We show that the problem of universality for unambiguous VASS is ExpSpace-complete, in sheer contrast to Ackermann-completeness for arbitrary VASS, even in dimension 1. When the dimension d is fixed, the universality problem is PSpace-complete if d is at least 2, and coNP-hard for 1-dimensional VASSes (also known as One Counter Nets).
△ Less
Submitted 21 July, 2020;
originally announced July 2020.
-
Parametrized Universality Problems for One-Counter Nets
Authors:
Shaull Almagor,
Udi Boker,
Piotr Hofman,
Patrick Totzke
Abstract:
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 questions: 1…
▽ More
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 questions: 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 problems 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.
△ Less
Submitted 4 July, 2020; v1 submitted 7 May, 2020;
originally announced May 2020.
-
Timed Basic Parallel Processes
Authors:
Lorenzo Clemente,
Piotr Hofman,
Patrick Totzke
Abstract:
Timed basic parallel processes (TBPP) extend communication-free Petri nets (aka. BPP or commutative context-free grammars) by a global notion of time. TBPP can be seen as an extension of timed automata (TA) with context-free branching rules, and as such may be used to model networks of independent timed automata with process creation.
We show that the coverability and reachability problems (with…
▽ More
Timed basic parallel processes (TBPP) extend communication-free Petri nets (aka. BPP or commutative context-free grammars) by a global notion of time. TBPP can be seen as an extension of timed automata (TA) with context-free branching rules, and as such may be used to model networks of independent timed automata with process creation.
We show that the coverability and reachability problems (with unary encoded target multiplicities) are PSPACE-complete and EXPTIME-complete, respectively. For the special case of 1-clock TBPP, both are NP-complete and hence not more complex than for untimed BPP. This contrasts with known super-Ackermannian-completeness and undecidability results for general timed Petri nets.
As a result of independent interest, and basis for our NP upper bounds, we show that the reachability relation of 1-clock TA can be expressed by a formula of polynomial size in the existential fragment of linear arithmetic, which improves on recent results from the literature.
△ Less
Submitted 8 July, 2019; v1 submitted 2 July, 2019;
originally announced July 2019.
-
Continuous Reachability for Unordered Data Petri nets is in PTime
Authors:
Utkarsh Gupta,
Preey Shah,
S. Akshay,
Piotr Hofman
Abstract:
Unordered data Petri nets (UDPN) are an extension of classical Petri nets with tokens that carry data from an infinite domain and where transitions may check equality and disequality of tokens. UDPN are well-structured, so the coverability and termination problems are decidable, but with higher complexity than for Petri nets. On the other hand, the problem of reachability for UDPN is surprisingly…
▽ More
Unordered data Petri nets (UDPN) are an extension of classical Petri nets with tokens that carry data from an infinite domain and where transitions may check equality and disequality of tokens. UDPN are well-structured, so the coverability and termination problems are decidable, but with higher complexity than for Petri nets. On the other hand, the problem of reachability for UDPN is surprisingly complex, and its decidability status remains open. In this paper, we consider the continuous reachability problem for UDPN, which can be seen as an over-approximation of the reachability problem. Our main result is a characterization of continuous reachability for UDPN and polynomial time algorithm for solving it. This is a consequence of a combinatorial argument, which shows that if continuous reachability holds then there exists a run using only polynomially many data values.
△ Less
Submitted 14 February, 2019;
originally announced February 2019.
-
Unboundedness problems for languages of vector addition systems
Authors:
Wojciech Czerwiński,
Piotr Hofman,
Georg Zetzsche
Abstract:
A vector addition system (VAS) with an initial and a final marking and transition labels induces a language. In part because the reachability problem in VAS remains far from being well-understood, it is difficult to devise decision procedures for such languages. This is especially true for checking properties that state the existence of infinitely many words of a particular shape. Informally, we c…
▽ More
A vector addition system (VAS) with an initial and a final marking and transition labels induces a language. In part because the reachability problem in VAS remains far from being well-understood, it is difficult to devise decision procedures for such languages. This is especially true for checking properties that state the existence of infinitely many words of a particular shape. Informally, we call these \emph{unboundedness properties}. We present a simple set of axioms for predicates that can express unboundedness properties. Our main result is that such a predicate is decidable for VAS languages as soon as it is decidable for regular languages. Among other results, this allows us to show decidability of (i)~separability by bounded regular languages, (ii)~unboundedness of occurring factors from a language $K$ with mild conditions on $K$, and (iii)~universality of the set of factors.
△ Less
Submitted 19 February, 2018;
originally announced February 2018.
-
Linear Equations with Ordered Data
Authors:
Piotr Hofman,
Sławomir Lasota
Abstract:
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 exponent…
▽ More
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.
△ Less
Submitted 19 February, 2018;
originally announced February 2018.
-
Bounding Average-energy Games
Authors:
Patricia Bouyer,
Piotr Hofman,
Nicolas Markey,
Mickael Randour,
Martin Zimmermann
Abstract:
We consider average-energy games, where the goal is to minimize the long-run average of the accumulated energy. While several results have been obtained on these games recently, decidability of average-energy games with a lower-bound constraint on the energy level (but no upper bound) remained open; in particular, so far there was no known upper bound on the memory that is required for winning str…
▽ More
We consider average-energy games, where the goal is to minimize the long-run average of the accumulated energy. While several results have been obtained on these games recently, decidability of average-energy games with a lower-bound constraint on the energy level (but no upper bound) remained open; in particular, so far there was no known upper bound on the memory that is required for winning strategies.
By reducing average-energy games with lower-bounded energy to infinite-state mean-payoff games and analyzing the density of low-energy configurations, we show an almost tight doubly-exponential upper bound on the necessary memory, and that the winner of average-energy games with lower-bounded energy can be determined in doubly-exponential time. We also prove EXPSPACE-hardness of this problem.
Finally, we consider multi-dimensional extensions of all types of average-energy games: without bounds, with only a lower bound, and with both a lower and an upper bound on the energy. We show that the fully-bounded version is the only case to remain decidable in multiple dimensions.
△ Less
Submitted 13 January, 2017; v1 submitted 25 October, 2016;
originally announced October 2016.
-
Linear Combinations of Unordered Data Vectors
Authors:
Piotr Hofman,
Jérôme Leroux,
Patrick Totzke
Abstract:
Data vectors generalise finite multisets: they are finitely supported functions into a commutative monoid. We study the question if a given data vector can be expressed as a finite sum of others, only assuming that 1) the domain is countable and 2) the given set of base vectors is finite up to permutations of the domain.
Based on a succinct representation of the involved permutations as integer…
▽ More
Data vectors generalise finite multisets: they are finitely supported functions into a commutative monoid. We study the question if a given data vector can be expressed as a finite sum of others, only assuming that 1) the domain is countable and 2) the given set of base vectors is finite up to permutations of the domain.
Based on a succinct representation of the involved permutations as integer linear constraints, we derive that positive instances can be witnessed in a bounded subset of the domain.
For data vectors over a group we moreover study when a data vector is reversible, that is, if its inverse is expressible using only nonnegative coefficients. We show that if all base vectors are reversible then the expressibility problem reduces to checking membership in finitely generated subgroups. Moreover, checking reversibility also reduces to such membership tests.
These questions naturally appear in the analysis of counter machines extended with unordered data: namely, for data vectors over $(\mathbb{Z}^d,+)$ expressibility directly corresponds to checking state equations for Coloured Petri nets where tokens can only be tested for equality. We derive that in this case, expressibility is in NP, and in P for reversible instances. These upper bounds are tight: they match the lower bounds for standard integer vectors (over singleton domains).
△ Less
Submitted 5 October, 2016;
originally announced October 2016.
-
Blind Friendly Maps: Tactile Maps for the Blind as a Part of the Public Map Portal (Mapy.cz)
Authors:
Petr Červenka,
Karel Břinda,
Michaela Hanousková,
Petr Hofman,
Radek Seifert
Abstract:
Blind people can now use maps located at Mapy.cz, thanks to the long-standing joint efforts of the ELSA Center at the Czech Technical University in Prague, the Teiresias Center at Masaryk University, and the company Seznam.cz. Conventional map underlays are automatically adjusted so that they could be read through touch after being printed on microcapsule paper, which opens a whole new perspective…
▽ More
Blind people can now use maps located at Mapy.cz, thanks to the long-standing joint efforts of the ELSA Center at the Czech Technical University in Prague, the Teiresias Center at Masaryk University, and the company Seznam.cz. Conventional map underlays are automatically adjusted so that they could be read through touch after being printed on microcapsule paper, which opens a whole new perspective in the use of tactile maps. Users may select an area of their choice in the Czech Republic (only within its boundaries, for the time being) and also the production of tactile maps, including the preparation of the map underlays, takes no more than several minutes.
△ Less
Submitted 31 March, 2016;
originally announced March 2016.
-
Complexity of regular abstractions of one-counter languages
Authors:
Mohamed Faouzi Atig,
Dmitry Chistikov,
Piotr Hofman,
K Narayan Kumar,
Prakash Saivasan,
Georg Zetzsche
Abstract:
We study the computational and descriptional complexity of the following transformation: Given a one-counter automaton (OCA) A, construct a nondeterministic finite automaton (NFA) B that recognizes an abstraction of the language L(A): its (1) downward closure, (2) upward closure, or (3) Parikh image.
For the Parikh image over a fixed alphabet and for the upward and downward closures, we find pol…
▽ More
We study the computational and descriptional complexity of the following transformation: Given a one-counter automaton (OCA) A, construct a nondeterministic finite automaton (NFA) B that recognizes an abstraction of the language L(A): its (1) downward closure, (2) upward closure, or (3) Parikh image.
For the Parikh image over a fixed alphabet and for the upward and downward closures, we find polynomial-time algorithms that compute such an NFA. For the Parikh image with the alphabet as part of the input, we find a quasi-polynomial time algorithm and prove a completeness result: we construct a sequence of OCA that admits a polynomial-time algorithm iff there is one for all OCA.
For all three abstractions, it was previously unknown if appropriate NFA of sub-exponential size exist.
△ Less
Submitted 10 February, 2016;
originally announced February 2016.
-
Simulation Problems Over One-Counter Nets
Authors:
Piotr Hofman,
Slawomir Lasota,
Richard Mayr,
Patrick Totzke
Abstract:
One-counter nets (OCN) are finite automata equipped with a counter that can store non-negative integer values, and that cannot be tested for zero. Equivalently, these are exactly 1-dimensional vector addition systems with states. We show that both strong and weak simulation preorder on OCN are PSPACE-complete.
One-counter nets (OCN) are finite automata equipped with a counter that can store non-negative integer values, and that cannot be tested for zero. Equivalently, these are exactly 1-dimensional vector addition systems with states. We show that both strong and weak simulation preorder on OCN are PSPACE-complete.
△ Less
Submitted 10 March, 2016; v1 submitted 1 February, 2016;
originally announced February 2016.
-
Shortest paths in one-counter systems
Authors:
Dmitry Chistikov,
Wojciech Czerwiński,
Piotr Hofman,
Michał Pilipczuk,
Michael Wehar
Abstract:
We show that any one-counter automaton with $n$ states, if its language is non-empty, accepts some word of length at most $O(n^2)$. This closes the gap between the previously known upper bound of $O(n^3)$ and lower bound of $Ω(n^2)$. More generally, we prove a tight upper bound on the length of shortest paths between arbitrary configurations in one-counter transition systems (weaker bounds have pr…
▽ More
We show that any one-counter automaton with $n$ states, if its language is non-empty, accepts some word of length at most $O(n^2)$. This closes the gap between the previously known upper bound of $O(n^3)$ and lower bound of $Ω(n^2)$. More generally, we prove a tight upper bound on the length of shortest paths between arbitrary configurations in one-counter transition systems (weaker bounds have previously appeared in the literature).
△ Less
Submitted 4 March, 2019; v1 submitted 19 October, 2015;
originally announced October 2015.
-
Tightening the Complexity of Equivalence Problems for Commutative Grammars
Authors:
Christoph Haase,
Piotr Hofman
Abstract:
We show that the language equivalence problem for regular and context-free commutative grammars is coNEXP-complete. In addition, our lower bound immediately yields further coNEXP-completeness results for equivalence problems for communication-free Petri nets and reversal-bounded counter automata. Moreover, we improve both lower and upper bounds for language equivalence for exponent-sensitive commu…
▽ More
We show that the language equivalence problem for regular and context-free commutative grammars is coNEXP-complete. In addition, our lower bound immediately yields further coNEXP-completeness results for equivalence problems for communication-free Petri nets and reversal-bounded counter automata. Moreover, we improve both lower and upper bounds for language equivalence for exponent-sensitive commutative grammars.
△ Less
Submitted 25 June, 2015;
originally announced June 2015.
-
Infinite-State Energy Games
Authors:
Parosh Aziz Abdulla,
Mohamed Faouzi Atig,
Piotr Hofman,
Richard Mayr,
K. Narayan Kumar,
Patrick Totzke
Abstract:
Energy games are a well-studied class of 2-player turn-based games on a finite graph where transitions are labeled with integer vectors which represent changes in a multidimensional resource (the energy). One player tries to keep the cumulative changes non-negative in every component while the other tries to frustrate this. We consider generalized energy games played on infinite game graphs induce…
▽ More
Energy games are a well-studied class of 2-player turn-based games on a finite graph where transitions are labeled with integer vectors which represent changes in a multidimensional resource (the energy). One player tries to keep the cumulative changes non-negative in every component while the other tries to frustrate this. We consider generalized energy games played on infinite game graphs induced by pushdown automata (modelling recursion) or their subclass of one-counter automata. Our main result is that energy games are decidable in the case where the game graph is induced by a one-counter automaton and the energy is one-dimensional. On the other hand, every further generalization is undecidable: Energy games on one-counter automata with a 2-dimensional energy are undecidable, and energy games on pushdown automata are undecidable even if the energy is one-dimensional. Furthermore, we show that energy games and simulation games are inter-reducible, and thus we additionally obtain several new (un)decidability results for the problem of checking simulation preorder between pushdown automata and vector addition systems.
△ Less
Submitted 3 May, 2014;
originally announced May 2014.
-
Trace Inclusion for One-Counter Nets Revisited
Authors:
Piotr Hofman,
Patrick Totzke
Abstract:
One-Counter nets (OCN) consist of a nondeterministic finite control and a single integer counter that cannot be fully tested for zero. They form a natural subclass of both One-Counter Automata, which allow zero-tests and Petri Nets/VASS, which allow multiple such weak counters.
The trace inclusion problem has recently been shown to be undecidable for OCN. In this paper, we contrast the complexit…
▽ More
One-Counter nets (OCN) consist of a nondeterministic finite control and a single integer counter that cannot be fully tested for zero. They form a natural subclass of both One-Counter Automata, which allow zero-tests and Petri Nets/VASS, which allow multiple such weak counters.
The trace inclusion problem has recently been shown to be undecidable for OCN. In this paper, we contrast the complexity of two natural restrictions which imply decidability.
First, we show that trace inclusion between an OCN and a deterministic OCN is NL-complete, even with arbitrary binary-encoded initial counter-values as part of the input. Secondly, we show Ackermannian completeness of for the trace universality problem of nondeterministic OCN. This problem is equivalent to checking trace inclusion between a finite and a OCN-process.
△ Less
Submitted 19 April, 2015; v1 submitted 21 April, 2014;
originally announced April 2014.
-
Simulation Over One-counter Nets is PSPACE-Complete
Authors:
Piotr Hofman,
Slawomir Lasota,
Richard Mayr,
Patrick Totzke
Abstract:
One-counter nets (OCN) are Petri nets with exactly one unbounded place. They are equivalent to a subclass of one-counter automata with just a weak test for zero. Unlike many other semantic equivalences, strong and weak simulation preorder are decidable for OCN, but the computational complexity was an open problem. We show that both strong and weak simulation preorder on OCN are PSPACE-complete.
One-counter nets (OCN) are Petri nets with exactly one unbounded place. They are equivalent to a subclass of one-counter automata with just a weak test for zero. Unlike many other semantic equivalences, strong and weak simulation preorder are decidable for OCN, but the computational complexity was an open problem. We show that both strong and weak simulation preorder on OCN are PSPACE-complete.
△ Less
Submitted 23 October, 2013;
originally announced October 2013.
-
Reachability Problem for Weak Multi-Pushdown Automata
Authors:
Wojciech Czerwiński,
Piotr Hofman,
SŁawomir Lasota
Abstract:
This paper is about reachability analysis in a restricted subclass of multi-pushdown automata. We assume that the control states of an automaton are partially ordered, and all transitions of an automaton go downwards with respect to the order. We prove decidability of the reachability problem, and computability of the backward reachability set. As the main contribution, we identify relevant subcl…
▽ More
This paper is about reachability analysis in a restricted subclass of multi-pushdown automata. We assume that the control states of an automaton are partially ordered, and all transitions of an automaton go downwards with respect to the order. We prove decidability of the reachability problem, and computability of the backward reachability set. As the main contribution, we identify relevant subclasses where the reachability problem becomes NP-complete. This matches the complexity of the same problem for communication-free vector addition systems, a special case of stateless multi-pushdown automata.
△ Less
Submitted 20 September, 2013; v1 submitted 19 August, 2013;
originally announced August 2013.
-
Decidability of Weak Simulation on One-counter Nets
Authors:
Piotr Hofman,
Richard Mayr,
Patrick Totzke
Abstract:
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 and that weak simulation approximants do not converge at level omega, but only at omega^2. In contrast, other semantic relations like weak bisimulation are undecidable for OCN, an…
▽ More
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 and that weak simulation approximants do not converge at level omega, but only at omega^2. In contrast, other semantic relations like weak bisimulation are undecidable for OCN, and so are weak (and strong) trace inclusion.
△ Less
Submitted 15 June, 2014; v1 submitted 15 April, 2013;
originally announced April 2013.
-
Approximating Weak Bisimilarity of Basic Parallel Processes
Authors:
Piotr Hofman,
Patrick Totzke
Abstract:
This paper explores the well known approximation approach to decide weak bisimilarity of Basic Parallel Processes. We look into how different refinement functions can be used to prove weak bisimilarity decidable for certain subclasses. We also show their limitations for the general case. In particular, we show a lower bound of ω \ast ω for the approximants which allow weak steps and a lower bound…
▽ More
This paper explores the well known approximation approach to decide weak bisimilarity of Basic Parallel Processes. We look into how different refinement functions can be used to prove weak bisimilarity decidable for certain subclasses. We also show their limitations for the general case. In particular, we show a lower bound of ω \ast ω for the approximants which allow weak steps and a lower bound of ω + ω for the approximants that allow sequences of actions. The former lower bound negatively answers the open question of Jančar and Hirshfeld.
△ Less
Submitted 13 August, 2012;
originally announced August 2012.
-
Relating timed and register automata
Authors:
Diego Figueira,
Piotr Hofman,
Sławomir Lasota
Abstract:
Timed automata and register automata are well-known models of computation over timed and data words respectively. The former has clocks that allow to test the lapse of time between two events, whilst the latter includes registers that can store data values for later comparison. Although these two models behave in appearance differently, several decision problems have the same (un)decidability an…
▽ More
Timed automata and register automata are well-known models of computation over timed and data words respectively. The former has clocks that allow to test the lapse of time between two events, whilst the latter includes registers that can store data values for later comparison. Although these two models behave in appearance differently, several decision problems have the same (un)decidability and complexity results for both models. As a prominent example, emptiness is decidable for alternating automata with one clock or register, both with non-primitive recursive complexity. This is not by chance.
This work confirms that there is indeed a tight relationship between the two models. We show that a run of a timed automaton can be simulated by a register automaton, and conversely that a run of a register automaton can be simulated by a timed automaton. Our results allow to transfer complexity and decidability results back and forth between these two kinds of models. We justify the usefulness of these reductions by obtaining new results on register automata.
△ Less
Submitted 29 November, 2010;
originally announced November 2010.
