Showing 1–40 of 40 results for author: Masopust, T

On Algorithms verifying Initial-and-Final-State Opacity: Complexity, Special Cases, and Comparison

Authors: Tomáš Masopust, Petr Osička

Abstract: Opacity is a general framework modeling security properties of systems interacting with a passive attacker. Initial-and-final-state opacity (IFO) generalizes the classical notions of opacity, such as current-state opacity and initial-state opacity. In IFO, the secret is whether the system evolved from a given initial state to a given final state or not. There are two algorithms for IFO verificatio… ▽ More Opacity is a general framework modeling security properties of systems interacting with a passive attacker. Initial-and-final-state opacity (IFO) generalizes the classical notions of opacity, such as current-state opacity and initial-state opacity. In IFO, the secret is whether the system evolved from a given initial state to a given final state or not. There are two algorithms for IFO verification. One arises from a trellis-based state estimator, which builds a semigroup of binary relations generated by the events of the automaton, and the other is based on the reduction to language inclusion. The time complexity of both algorithms is bounded by a super-exponential function, and it is a challenging open problem to find a faster algorithm or to show that no faster algorithm exists. We discuss the lower-bound time complexity for both general and special cases, and use extensive benchmarks to compare the existing algorithms. △ Less

Submitted 24 December, 2024; v1 submitted 26 February, 2024; originally announced February 2024.

Speed Me up if You Can: Conditional Lower Bounds on Opacity Verification

Authors: Jiří Balun, Tomáš Masopust, Petr Osička

Abstract: Opacity is a property of privacy and security applications asking whether, given a system model, a passive intruder that makes online observations of system's behaviour can ascertain some "secret" information of the system. Deciding opacity is a PSpace-complete problem, and hence there are no polynomial-time algorithms to verify opacity under the assumption that PSpace differs from PTime. This ass… ▽ More Opacity is a property of privacy and security applications asking whether, given a system model, a passive intruder that makes online observations of system's behaviour can ascertain some "secret" information of the system. Deciding opacity is a PSpace-complete problem, and hence there are no polynomial-time algorithms to verify opacity under the assumption that PSpace differs from PTime. This assumption, however, gives rise to a question whether the existing exponential-time algorithms are the best possible or whether there are faster, sub-exponential-time algorithms. We show that under the (Strong) Exponential Time Hypothesis, there are no algorithms that would be significantly faster than the existing algorithms. As a by-product, we obtained a new conditional lower bound on the time complexity of deciding universality (and therefore also inclusion and equivalence) for nondeterministic finite automata. △ Less

Submitted 19 April, 2023; originally announced April 2023.

Supervisory Control of Modular Discrete-Event Systems under Partial Observation: Normality

Authors: Jan Komenda, Tomáš Masopust

Abstract: Complex systems are often composed of many small communicating components called modules. We investigate the synthesis of supervisory controllers for modular systems under partial observation that, as the closed-loop system, realize the supremal normal sublanguage of the specification. We call such controllers maximally permissive normal supervisors. The challenge in modular systems is to find con… ▽ More Complex systems are often composed of many small communicating components called modules. We investigate the synthesis of supervisory controllers for modular systems under partial observation that, as the closed-loop system, realize the supremal normal sublanguage of the specification. We call such controllers maximally permissive normal supervisors. The challenge in modular systems is to find conditions under which the global nonblocking and maximally permissive normal supervisor can be achieved locally as the parallel composition of local normal supervisors. We show that a structural concept of hierarchical supervisory control called modified observation consistency (MOC) is such a condition. However, the algorithmic verification of MOC is an open problem, and therefore it is necessary to find easily-verifiable conditions that ensure MOC. We show that the condition that all shared events are observable is such a condition. Considering specifications, we examine both local specifications, where each module has its own specification, and global specifications. We combine our results for normality with the existing results for controllability to locally synthesize the nonblocking and maximally permissive controllable and normal supervisor. Finally, we illustrate the results on an industrial case study of the patient table of an MRI scanner. △ Less

Submitted 21 February, 2023; originally announced February 2023.

K-Step Opacity in Discrete Event Systems: Verification, Complexity, and Relations

Authors: Jiří Balun, Tomáš Masopust

Abstract: Opacity is a property expressing whether a system may reveal its secret to a passive observer (an intruder) who knows the structure of the system but has a limited observation of its behavior. Several notions of opacity have been studied, including current-state opacity, K-step opacity, and infinite-step opacity. We study K-step opacity that generalizes both current-state opacity and infinite-step… ▽ More Opacity is a property expressing whether a system may reveal its secret to a passive observer (an intruder) who knows the structure of the system but has a limited observation of its behavior. Several notions of opacity have been studied, including current-state opacity, K-step opacity, and infinite-step opacity. We study K-step opacity that generalizes both current-state opacity and infinite-step opacity, and asks whether the intruder cannot decide, at any time, whether or when the system was in a secret state during the last K observable steps. We design a new algorithm deciding K-step opacity the complexity of which is lower than that of existing algorithms and that does not depend on K. We then compare K-step opacity with other opacity notions and provide new transformations among the notions that do not use states that are neither secret nor non-secret (neutral states) and that are polynomial with respect to both the size of the system and the binary encoding of K. △ Less

Submitted 5 September, 2021; originally announced September 2021.

Comparing the Notions of Opacity for Discrete-Event Systems

Authors: Jiří Balun, Tomáš Masopust

Abstract: Opacity is an information flow property characterizing whether a system reveals its secret to a passive observer. Several notions of opacity have been introduced in the literature. We study the notions of language-based opacity, current-state opacity, initial-state opacity, initial-and-final-state opacity, K-step opacity, and infinite-step opacity. Comparing the notions is a natural question that… ▽ More Opacity is an information flow property characterizing whether a system reveals its secret to a passive observer. Several notions of opacity have been introduced in the literature. We study the notions of language-based opacity, current-state opacity, initial-state opacity, initial-and-final-state opacity, K-step opacity, and infinite-step opacity. Comparing the notions is a natural question that has been investigated and summarized by Wu and Lafortune, who provided transformations among current-state opacity, initial-and-final-state opacity, and language-based opacity, and, for prefix-closed languages, also between language-based opacity and initial-state opacity. We extend these results by showing that all the discussed notions of opacity are transformable to each other. Besides a deeper insight into the differences among the notions, the transformations have applications in complexity results. In particular, the transformations are computable in polynomial time and preserve the number of observable events and determinism, and hence the computational complexities of the verification of the notions coincide. We provide a complete and improved complexity picture of the verification of the discussed notions of opacity, and improve the algorithmic complexity of deciding language-based opacity, infinite-step opacity, and K-step opacity. △ Less

Submitted 26 June, 2021; v1 submitted 4 February, 2021; originally announced February 2021.

On Opacity Verification for Discrete-Event Systems

Authors: Jiří Balun, Tomáš Masopust

Abstract: Opacity is an information flow property characterizing whether a system reveals its secret to an intruder. Verification of opacity for discrete-event systems modeled by automata is in general a hard problem. We discuss the question whether there are structural restrictions on the system models for which the opacity verification is tractable. We consider two kinds of automata models: (i) acyclic au… ▽ More Opacity is an information flow property characterizing whether a system reveals its secret to an intruder. Verification of opacity for discrete-event systems modeled by automata is in general a hard problem. We discuss the question whether there are structural restrictions on the system models for which the opacity verification is tractable. We consider two kinds of automata models: (i) acyclic automata, and (ii) automata where all cycles are only in the form of self-loops. In some sense, these models are the simplest models of (deadlock-free) systems. Although the expressivity of such systems is weaker than the expressivity of linear temporal logic, we show that the opacity verification for these systems is still hard. △ Less

Submitted 16 December, 2019; originally announced December 2019.

On Verification of D-Detectability for Discrete Event Systems

Authors: Jiří Balun, Tomáš Masopust

Abstract: Detectability has been introduced as a generalization of state-estimation properties of discrete event systems studied in the literature. It asks whether the current and subsequent states of a system can be determined based on observations. Since, in some applications, to exactly determine the current and subsequent states may be too strict, a relaxed notion of D-detectability has been introduced,… ▽ More Detectability has been introduced as a generalization of state-estimation properties of discrete event systems studied in the literature. It asks whether the current and subsequent states of a system can be determined based on observations. Since, in some applications, to exactly determine the current and subsequent states may be too strict, a relaxed notion of D-detectability has been introduced, distinguishing only certain pairs of states rather than all states. Four variants of D-detectability have been defined: strong (periodic) D-detectability and weak (periodic) D-detectability. Deciding weak (periodic) D-detectability is PSpace-complete, while deciding strong (periodic) detectability or strong D-detectability is polynomial (and we show that it is actually NL-complete). However, to the best of our knowledge, it is an open problem whether there exists a polynomial-time algorithm deciding strong periodic D-detectability. We solve this problem by showing that deciding strong periodic D-detectability is a PSpace-complete problem, and hence there is no polynomial-time algorithm unless PSpace = P. We further show that there is no polynomial-time algorithm deciding strong periodic D-detectability even for systems with a single observable event, unless P = NP. Finally, we propose a class of systems for which the problem is tractable. △ Less

Submitted 16 May, 2020; v1 submitted 16 December, 2019; originally announced December 2019.

Comments: Extended version of a paper accepted for WODES 2020

Conditions for Hierarchical Supervisory Control under Partial Observation

Authors: Jan Komenda, Tomáš Masopust

Abstract: The fundamental problem in hierarchical supervisory control under partial observation is to find conditions preserving observability between the original (low-level) and the abstracted (high-level) plants. Two conditions for observable specifications were identified in the literature -- observation consistency (OC) and local observation consistency (LOC). However, the decidability of OC and LOC we… ▽ More The fundamental problem in hierarchical supervisory control under partial observation is to find conditions preserving observability between the original (low-level) and the abstracted (high-level) plants. Two conditions for observable specifications were identified in the literature -- observation consistency (OC) and local observation consistency (LOC). However, the decidability of OC and LOC were left open. We show that both OC and LOC are decidable for regular systems. We further show that these conditions do not guarantee that supremal (normal or relatively observable) sublanguages computed on the low level and on the high level always coincide. To solve the issue, we suggest a new condition -- modified observation consistency -- and show that under this condition, the supremal normal sublanguages are preserved between the levels, while the supremal relatively observable high-level sublanguage is at least as good as the supremal relatively observable low-level sublanguage, i.e., the high-level solution may be even better than the low-level solution. △ Less

Submitted 10 March, 2023; v1 submitted 16 December, 2019; originally announced December 2019.

Comments: We have added the errata to some statements that are not correct as stated in the paper

Partially Ordered Automata and Piecewise Testability

Authors: Tomáš Masopust, Markus Krötzsch

Abstract: Partially ordered automata are automata where the transition relation induces a partial order on states. The expressive power of partially ordered automata is closely related to the expressivity of fragments of first-order logic on finite words or, equivalently, to the language classes of the levels of the Straubing-Thérien hierarchy. Several fragments (levels) have been intensively investigated u… ▽ More Partially ordered automata are automata where the transition relation induces a partial order on states. The expressive power of partially ordered automata is closely related to the expressivity of fragments of first-order logic on finite words or, equivalently, to the language classes of the levels of the Straubing-Thérien hierarchy. Several fragments (levels) have been intensively investigated under various names. For instance, the fragment of first-order formulae with a single existential block of quantifiers in prenex normal form is known as piecewise testable languages or $J$-trivial languages. These languages are characterized by confluent partially ordered DFAs or by complete, confluent, and self-loop-deterministic partially ordered NFAs (ptNFAs for short). In this paper, we study the complexity of basic questions for several types of partially ordered automata on finite words; namely, the questions of inclusion, equivalence, and ($k$-)piecewise testability. The lower-bound complexity boils down to the complexity of universality. The universality problem asks whether a system recognizes all words over its alphabet. For ptNFAs, the complexity of universality decreases if the alphabet is fixed, but it is open if the alphabet may grow with the number of states. We show that deciding universality for general ptNFAs is as hard as for general NFAs. Our proof is a novel and nontrivial extension of our recent construction for self-loop-deterministic partially ordered NFAs, a model strictly more expressive than ptNFAs. We provide a comprehensive picture of the complexities of the problems of inclusion, equivalence, and ($k$-)piecewise testability for the considered types of automata. △ Less

Submitted 10 May, 2021; v1 submitted 29 July, 2019; originally announced July 2019.

Comments: arXiv admin note: text overlap with arXiv:1704.07860

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 2 (May 11, 2021) lmcs:5900

Critical Observability for Automata and Petri Nets

Authors: Tomáš Masopust

Abstract: Critical observability is a property of cyber-physical systems to detect whether the current state belongs to a set of critical states. In safety-critical applications, critical states model operations that may be unsafe or of a particular interest. De Santis et al. introduced critical observability for linear switching systems, and Pola et al. adapted it for discrete-event systems, focusing on al… ▽ More Critical observability is a property of cyber-physical systems to detect whether the current state belongs to a set of critical states. In safety-critical applications, critical states model operations that may be unsafe or of a particular interest. De Santis et al. introduced critical observability for linear switching systems, and Pola et al. adapted it for discrete-event systems, focusing on algorithmic complexity. We study the computational complexity of deciding critical observability for systems modeled as (networks of) finite-state automata and Petri nets. We show that deciding critical observability is (i) NL-complete for finite automata, that is, it is efficiently verifiable on parallel computers, (ii) PSPACE-complete for networks of finite automata, that is, it is very unlikely solvable in polynomial time, and (iii) undecidable for labeled Petri nets, but becoming decidable if the set of critical states (markings) is finite or co-finite, in which case the problem is as hard as the non-reachability problem for Petri nets. △ Less

Submitted 17 April, 2019; v1 submitted 1 August, 2018; originally announced August 2018.

Comments: Accepted for publication in IEEE TAC

MSC Class: 93C65; 68Q25; 68Q45;

Automatic Generation of Optimal Reductions of Distributions

Authors: Liyong Lin, Tomáš Masopust, W. Murray Wonham, Rong Su

Abstract: A reduction of a source distribution is a collection of smaller sized distributions that are collectively equivalent to the source distribution with respect to the property of decomposability. That is, an arbitrary language is decomposable with respect to the source distribution if and only if it is decomposable with respect to each smaller sized distribution (in the reduction). The notion of redu… ▽ More A reduction of a source distribution is a collection of smaller sized distributions that are collectively equivalent to the source distribution with respect to the property of decomposability. That is, an arbitrary language is decomposable with respect to the source distribution if and only if it is decomposable with respect to each smaller sized distribution (in the reduction). The notion of reduction of distributions has previously been proposed to improve the complexity of decomposability verification. In this work, we address the problem of generating (optimal) reductions of distributions automatically. A (partial) solution to this problem is provided, which consists of 1) an incremental algorithm for the production of candidate reductions and 2) a reduction validation procedure. In the incremental production stage, backtracking is applied whenever a candidate reduction that cannot be validated is produced. A strengthened substitution-based proof technique is used for reduction validation, while a fixed template of candidate counter examples is used for reduction refutation; put together, they constitute our (partial) solution to the reduction verification problem. In addition, we show that a recursive approach for the generation of (small) reductions is easily supported. △ Less

Submitted 29 March, 2018; originally announced March 2018.

Comments: Accepted for publication in IEEE Transactions on Automatic Control

Deciding Detectability for Labeled Petri Nets

Authors: Tomas Masopust, Xiang Yin

Abstract: Detectability of discrete event systems (DESs) is a property to determine a priori whether the current and subsequent states can be determined based on observations. In this paper, we investigate the verification of two detectability properties -- strong detectability and weak detectability -- for DESs modeled by labeled Petri nets. Strong detectability requires that we can always determine, after… ▽ More Detectability of discrete event systems (DESs) is a property to determine a priori whether the current and subsequent states can be determined based on observations. In this paper, we investigate the verification of two detectability properties -- strong detectability and weak detectability -- for DESs modeled by labeled Petri nets. Strong detectability requires that we can always determine, after a finite number of observations, the current and subsequent markings of the system, while weak detectability requires that we can determine, after a finite number of observations, the current and subsequent markings for some trajectories of the system. We show that for DESs modeled by labeled Petri nets, checking strong detectability is decidable whereas checking weak detectability is undecidable. Our results extend the existing studies on the verification of detectability from finite-state automata to labeled Petri nets. As a consequence, we strengthen a result on checking current-state opacity for labeled Petri nets. △ Less

Submitted 29 November, 2018; v1 submitted 6 February, 2018; originally announced February 2018.

Complexity of Detectability, Opacity and A-Diagnosability for Modular Discrete Event Systems

Authors: Tomáš Masopust, Xiang Yin

Abstract: We study the complexity of deciding whether a modular discrete event system is detectable (resp. opaque, A-diagnosable). Detectability arises in the state estimation of discrete event systems, opacity is related to the privacy and security analysis, and A-diagnosability appears in the fault diagnosis of stochastic discrete event systems. Previously, deciding weak detectability (opacity, A-diagnosa… ▽ More We study the complexity of deciding whether a modular discrete event system is detectable (resp. opaque, A-diagnosable). Detectability arises in the state estimation of discrete event systems, opacity is related to the privacy and security analysis, and A-diagnosability appears in the fault diagnosis of stochastic discrete event systems. Previously, deciding weak detectability (opacity, A-diagnosability) for monolithic systems was shown to be PSPACE-complete. In this paper, we study the complexity of deciding weak detectability (opacity, A-diagnosability) for modular systems. We show that the complexities of these problems are significantly worse than in the monolithic case. Namely, we show that deciding modular weak detectability (opacity, A-diagnosability) is EXPSPACE-complete. We further discuss a special case where all unobservable events are private, and show that in this case the problems are PSPACE-complete. Consequently, if the systems are all fully observable, then deciding weak detectability (opacity) for modular systems is PSPACE-complete. △ Less

Submitted 8 October, 2017; originally announced October 2017.

Complexity of Deciding Detectability in Discrete Event Systems

Authors: Tomáš Masopust

Abstract: Detectability of discrete event systems (DESs) is a question whether the current and subsequent states can be determined based on observations. Shu and Lin designed a polynomial-time algorithm to check strong (periodic) detectability and an exponential-time (polynomial-space) algorithm to check weak (periodic) detectability. Zhang showed that checking weak (periodic) detectability is PSpace-comple… ▽ More Detectability of discrete event systems (DESs) is a question whether the current and subsequent states can be determined based on observations. Shu and Lin designed a polynomial-time algorithm to check strong (periodic) detectability and an exponential-time (polynomial-space) algorithm to check weak (periodic) detectability. Zhang showed that checking weak (periodic) detectability is PSpace-complete. This intractable complexity opens a question whether there are structurally simpler DESs for which the problem is tractable. In this paper, we show that it is not the case by considering DESs represented as deterministic finite automata without non-trivial cycles, which are structurally the simplest deadlock-free DESs. We show that even for such very simple DESs, checking weak (periodic) detectability remains intractable. On the contrary, we show that strong (periodic) detectability of DESs can be efficiently verified on a parallel computer. △ Less

Submitted 6 October, 2017; originally announced October 2017.

On the Height of Towers of Subsequences and Prefixes

Authors: Štěpán Holub, Tomáš Masopust, Michaël Thomazo

Abstract: A tower is a sequence of words alternating between two languages in such a way that every word is a subsequence of the following word. The height of the tower is the number of words in the sequence. If there is no infinite tower (a tower of infinite height), then the height of all towers between the languages is bounded. We study upper and lower bounds on the height of maximal finite towers with r… ▽ More A tower is a sequence of words alternating between two languages in such a way that every word is a subsequence of the following word. The height of the tower is the number of words in the sequence. If there is no infinite tower (a tower of infinite height), then the height of all towers between the languages is bounded. We study upper and lower bounds on the height of maximal finite towers with respect to the size of the NFA (the DFA) representation of the languages. We show that the upper bound is polynomial in the number of states and exponential in the size of the alphabet, and that it is asymptotically tight if the size of the alphabet is fixed. If the alphabet may grow, then, using an alphabet of size approximately the number of states of the automata, the lower bound on the height of towers is exponential with respect to that number. In this case, there is a gap between the lower and upper bound, and the asymptotically optimal bound remains an open problem. Since, in many cases, the constructed towers are sequences of prefixes, we also study towers of prefixes. △ Less

Submitted 8 May, 2017; originally announced May 2017.

MSC Class: 68R05; 68Q45

Journal ref: Information and Computation 265 (2019) 77-93

Universality of Confluent, Self-Loop Deterministic Partially Ordered NFAs is Hard

Authors: Tomáš Masopust, Markus Krötzsch

Abstract: An automaton is partially ordered if the only cycles in its transition diagram are self-loops. The expressivity of partially ordered NFAs (poNFAs) can be characterized by the Straubing-Thérien hierarchy. Level 3/2 is recognized by poNFAs, level 1 by confluent, self-loop deterministic poNFAs as well as by confluent poDFAs, and level 1/2 by saturated poNFAs. We study the universality problem for con… ▽ More An automaton is partially ordered if the only cycles in its transition diagram are self-loops. The expressivity of partially ordered NFAs (poNFAs) can be characterized by the Straubing-Thérien hierarchy. Level 3/2 is recognized by poNFAs, level 1 by confluent, self-loop deterministic poNFAs as well as by confluent poDFAs, and level 1/2 by saturated poNFAs. We study the universality problem for confluent, self-loop deterministic poNFAs. It asks whether an automaton accepts all words over its alphabet. Universality for both NFAs and poNFAs is a PSpace-complete problem. For confluent, self-loop deterministic poNFAs, the complexity drops to coNP-complete if the alphabet is fixed but is open if the alphabet may grow. We solve this problem by showing that it is PSpace-complete if the alphabet may grow polynomially. Consequently, our result provides a lower-bound complexity for some other problems, including inclusion, equivalence, and $k$-piecewise testability. Since universality for saturated poNFAs is easy, confluent, self-loop deterministic poNFAs are the simplest and natural kind of NFAs characterizing a well-known class of languages, for which deciding universality is as difficult as for general NFAs. △ Less

Submitted 25 April, 2017; originally announced April 2017.

Comments: arXiv admin note: text overlap with arXiv:1609.03460

Separability by Piecewise Testable Languages is PTime-Complete

Authors: Tomáš Masopust

Abstract: Piecewise testable languages form the first level of the Straubing-Thérien hierarchy. The membership problem for this level is decidable and testing if the language of a DFA is piecewise testable is NL-complete. The question has not yet been addressed for NFAs. We fill in this gap by showing that it is PSpace-complete. The main result is then the lower-bound complexity of separability of regular l… ▽ More Piecewise testable languages form the first level of the Straubing-Thérien hierarchy. The membership problem for this level is decidable and testing if the language of a DFA is piecewise testable is NL-complete. The question has not yet been addressed for NFAs. We fill in this gap by showing that it is PSpace-complete. The main result is then the lower-bound complexity of separability of regular languages by piecewise testable languages. Two regular languages are separable by a piecewise testable language if the piecewise testable language includes one of them and is disjoint from the other. For languages represented by NFAs, separability by piecewise testable languages is known to be decidable in PTime. We show that it is PTime-hard and that it remains PTime-hard even for minimal DFAs. △ Less

Submitted 17 November, 2017; v1 submitted 25 April, 2017; originally announced April 2017.

Comments: Revised version of related results separated from arXiv:1409.3943

MSC Class: 68Q45; 68Q17; 68Q25; 03D05

Complexity of Infimal Observable Superlanguages

Authors: Tomáš Masopust

Abstract: The infimal prefix-closed, controllable and observable superlanguage plays an essential role in the relationship between controllability, observability and co-observability -- the central notions of supervisory control theory. Existing algorithms for its computation are exponential and it is not known whether a polynomial algorithm exists. In this paper, we study the state complexity of this langu… ▽ More The infimal prefix-closed, controllable and observable superlanguage plays an essential role in the relationship between controllability, observability and co-observability -- the central notions of supervisory control theory. Existing algorithms for its computation are exponential and it is not known whether a polynomial algorithm exists. In this paper, we study the state complexity of this language. State complexity of a language is the number of states of the minimal DFA for the language. For a language of state complexity $n$, we show that the upper-bound state complexity on the infimal prefix-closed and observable superlanguage is $2^n + 1$ and that this bound is asymptotically tight. It proves that there is no algorithm computing a DFA of the infimal prefix-closed and observable superlanguage in polynomial time. Our construction further shows that such a DFA can be computed in time $O(2^n)$. The construction involves NFAs and a computation of the supremal prefix-closed sublanguage. We study the computation of the supremal prefix-closed sublanguage and show that there is no polynomial-time algorithm that computes an NFA of the supremal prefix-closed sublanguage of a language given as an NFA even if the language is unary. △ Less

Submitted 15 March, 2017; originally announced March 2017.

Complexity of Verifying Nonblockingness in Modular Supervisory Control

Authors: Tomáš Masopust

Abstract: Complexity analysis becomes a common task in supervisory control. However, many results of interest are spread across different topics. The aim of this paper is to bring several interesting results from complexity theory and to illustrate their relevance to supervisory control by proving new nontrivial results concerning nonblockingness in modular supervisory control of discrete event systems mode… ▽ More Complexity analysis becomes a common task in supervisory control. However, many results of interest are spread across different topics. The aim of this paper is to bring several interesting results from complexity theory and to illustrate their relevance to supervisory control by proving new nontrivial results concerning nonblockingness in modular supervisory control of discrete event systems modeled by finite automata. △ Less

Submitted 15 March, 2017; originally announced March 2017.

Complexity of Universality and Related Problems for Partially Ordered NFAs

Authors: Markus Krötzsch, Tomáš Masopust, Michaël Thomazo

Abstract: Partially ordered nondeterminsitic finite automata (poNFAs) are NFAs whose transition relation induces a partial order on states, that is, for which cycles occur only in the form of self-loops on a single state. A poNFA is universal if it accepts all words over its input alphabet. Deciding universality is PSPACE-complete for poNFAs, and we show that this remains true even when restricting to a fix… ▽ More Partially ordered nondeterminsitic finite automata (poNFAs) are NFAs whose transition relation induces a partial order on states, that is, for which cycles occur only in the form of self-loops on a single state. A poNFA is universal if it accepts all words over its input alphabet. Deciding universality is PSPACE-complete for poNFAs, and we show that this remains true even when restricting to a fixed alphabet. This is nontrivial since standard encodings of alphabet symbols in, e.g., binary can turn self-loops into longer cycles. A lower coNP-complete complexity bound can be obtained if we require that all self-loops in the poNFA are deterministic, in the sense that the symbol read in the loop cannot occur in any other transition from that state. We find that such restricted poNFAs (rpoNFAs) characterise the class of $\mathcal{R}$-trivial languages, and we establish the complexity of deciding if the language of an NFA is $\mathcal{R}$-trivial. Nevertheless, the limitation to fixed alphabets turns out to be essential even in the restricted case: deciding universality of rpoNFAs with unbounded alphabets is PSPACE-complete. Based on a close relation between universality and the problems of inclusion and equivalence, we also obtain the complexity results for these two problems. Finaly, we show that the languages of rpoNFAs are definable by deterministic (one-unambiguous) regular expressions, which makes them interesting in schema languages for XML data. △ Less

Submitted 23 June, 2017; v1 submitted 12 September, 2016; originally announced September 2016.

Comments: Preliminary version presented at MFCS 2016

Journal ref: Information and Computation, 255, Part 1, 177-192, 2017

On a Distributed Computation of Supervisors in Modular Supervisory Control

Authors: Jan Komenda, Tomáš Masopust, J. H. van Schuppen

Abstract: In this paper, we discuss a supervisory control problem of modular discrete-event systems that allows for a distributed computation of supervisors. We provide a characterization and an algorithm to compute the supervisors. If the specification does not satisfy the properties, we make use of a relaxation of coordination control to compute a sublanguage of the specification for which the supervisors… ▽ More In this paper, we discuss a supervisory control problem of modular discrete-event systems that allows for a distributed computation of supervisors. We provide a characterization and an algorithm to compute the supervisors. If the specification does not satisfy the properties, we make use of a relaxation of coordination control to compute a sublanguage of the specification for which the supervisors can be computed in a distributed way. △ Less

Submitted 6 September, 2016; originally announced September 2016.

Comments: Extended abstract of a paper presented at the International Conference on Complex Systems Engineering (ICCSE 2015)

Piecewise Testable Languages and Nondeterministic Automata

Authors: Tomáš Masopust

Abstract: A regular language is $k$-piecewise testable if it is a finite boolean combination of languages of the form $Σ^* a_1 Σ^* \cdots Σ^* a_n Σ^*$, where $a_i\inΣ$ and $0\le n \le k$. Given a DFA $A$ and $k\ge 0$, it is an NL-complete problem to decide whether the language $L(A)$ is piecewise testable and, for $k\ge 4$, it is coNP-complete to decide whether the language $L(A)$ is $k$-piecewise testable.… ▽ More A regular language is $k$-piecewise testable if it is a finite boolean combination of languages of the form $Σ^* a_1 Σ^* \cdots Σ^* a_n Σ^*$, where $a_i\inΣ$ and $0\le n \le k$. Given a DFA $A$ and $k\ge 0$, it is an NL-complete problem to decide whether the language $L(A)$ is piecewise testable and, for $k\ge 4$, it is coNP-complete to decide whether the language $L(A)$ is $k$-piecewise testable. It is known that the depth of the minimal DFA serves as an upper bound on $k$. Namely, if $L(A)$ is piecewise testable, then it is $k$-piecewise testable for $k$ equal to the depth of $A$. In this paper, we show that some form of nondeterminism does not violate this upper bound result. Specifically, we define a class of NFAs, called ptNFAs, that recognize piecewise testable languages and show that the depth of a ptNFA provides an (up to exponentially better) upper bound on $k$ than the minimal DFA. We provide an application of our result, discuss the relationship between $k$-piecewise testability and the depth of NFAs, and study the complexity of $k$-piecewise testability for ptNFAs. △ Less

Submitted 10 March, 2016; v1 submitted 1 March, 2016; originally announced March 2016.

Comments: Corrections in section 4.1

ACM Class: F.1.1; F.4.3

Computation of Controllable and Coobservable Sublanguages in Decentralized Supervisory Control via Communication

Authors: Jan Komenda, Tomáš Masopust

Abstract: In decentralized supervisory control, several local supervisors cooperate to accomplish a common goal (specification). Controllability and coobservability are the key conditions to achieve a specification in the controlled system. We construct a controllable and coobservable sublanguage of the specification by using additional communications between supervisors. Namely, we extend observable events… ▽ More In decentralized supervisory control, several local supervisors cooperate to accomplish a common goal (specification). Controllability and coobservability are the key conditions to achieve a specification in the controlled system. We construct a controllable and coobservable sublanguage of the specification by using additional communications between supervisors. Namely, we extend observable events of local supervisors via communication and apply a fully decentralized computation of local supervisors. Coobservability is then guaranteed by construction. Sufficient conditions to achieve the centralized optimal solution are discussed. Our approach can be used for both prefix-closed and non-prefix-closed specifications. △ Less

Submitted 25 January, 2017; v1 submitted 10 December, 2015; originally announced December 2015.

Journal ref: Discrete Event Dynamic Systems, 27(4), 585-608, 2017

On $k$-piecewise testability (preliminary report)

Authors: Tomáš Masopust, Michaël Thomazo

Abstract: For a non-negative integer $k$, a language is $k$-piecewise test\-able ($k$-PT) if it is a finite boolean combination of languages of the form $Σ^* a_1 Σ^* \cdots Σ^* a_n Σ^*$ for $a_i\inΣ$ and $0\le n \le k$. We study the following problem: Given a DFA recognizing a piecewise testable language, decide whether the language is $k$-PT. We provide a complexity bound and a detailed analysis for small… ▽ More For a non-negative integer $k$, a language is $k$-piecewise test\-able ($k$-PT) if it is a finite boolean combination of languages of the form $Σ^* a_1 Σ^* \cdots Σ^* a_n Σ^*$ for $a_i\inΣ$ and $0\le n \le k$. We study the following problem: Given a DFA recognizing a piecewise testable language, decide whether the language is $k$-PT. We provide a complexity bound and a detailed analysis for small $k$'s. The result can be used to find the minimal $k$ for which the language is $k$-PT. We show that the upper bound on $k$ given by the depth of the minimal DFA can be exponentially bigger than the minimal possible $k$, and provide a tight upper bound on the depth of the minimal DFA recognizing a $k$-PT language. △ Less

Submitted 9 June, 2015; v1 submitted 4 December, 2014; originally announced December 2014.

Comments: Full version of the paper accepted for DLT 2015

Alternating Towers and Piecewise Testable Separators

Authors: Štěpán Holub, Tomáš Masopust, Michaël Thomazo

Abstract: Two languages are separable by a piecewise testable language if and only if there exists no infinite tower between them. An infinite tower is an infinite sequence of strings alternating between the two languages such that every string is a subsequence (scattered substring) of all the strings that follow. For regular languages represented by nondeterministic finite automata, the existence of an inf… ▽ More Two languages are separable by a piecewise testable language if and only if there exists no infinite tower between them. An infinite tower is an infinite sequence of strings alternating between the two languages such that every string is a subsequence (scattered substring) of all the strings that follow. For regular languages represented by nondeterministic finite automata, the existence of an infinite tower is decidable in polynomial time. In this paper, we investigate the complexity of a particular method to compute a piecewise testable separator. We show that it is closely related to the height of maximal finite towers, and provide the upper and lower bounds with respect to the size of the given nondeterministic automata. Specifically, we show that the upper bound is polynomial with respect to the number of states with the cardinality of the alphabet in the exponent. Concerning the lower bound, we show that towers of exponential height with respect to the cardinality of the alphabet exist. Since these towers mostly turn out to be sequences of prefixes, we also provide a comparison with towers of prefixes. △ Less

Submitted 12 November, 2015; v1 submitted 13 September, 2014; originally announced September 2014.

Comments: Update on the state complexity of AFAs under the operation of downward closure

MSC Class: 68Q45; 68Q17; 68Q25; 03D05

On Upper and Lower Bounds on the Length of Alternating Towers

Authors: Štěpán Holub, Galina Jirásková, Tomáš Masopust

Abstract: A tower between two regular languages is a sequence of strings such that all strings on odd positions belong to one of the languages, all strings on even positions belong to the other language, and each string can be embedded into the next string in the sequence. It is known that if there are towers of any length, then there also exists an infinite tower. We investigate upper and lower bounds on t… ▽ More A tower between two regular languages is a sequence of strings such that all strings on odd positions belong to one of the languages, all strings on even positions belong to the other language, and each string can be embedded into the next string in the sequence. It is known that if there are towers of any length, then there also exists an infinite tower. We investigate upper and lower bounds on the length of finite towers between two regular languages with respect to the size of the automata representing the languages in the case there is no infinite tower. This problem is relevant to the separation problem of regular languages by piecewise testable languages. △ Less

Submitted 9 July, 2014; v1 submitted 17 April, 2014; originally announced April 2014.

Journal ref: MFCS 2014, LNCS 8634, pp. 315-326

A Note on Relative Observability in Coordination Control

Authors: Jan Komenda, Tomáš Masopust, Jan H. van Schuppen

Abstract: Relative observability has been introduced and studied in the framework of partially observed discrete-event systems as a condition stronger than observability, but weaker than normality. However, unlike observability, relative observability is closed under language unions, which makes it interesting for practical applications. In this paper, we investigate this notion in the framework of coordina… ▽ More Relative observability has been introduced and studied in the framework of partially observed discrete-event systems as a condition stronger than observability, but weaker than normality. However, unlike observability, relative observability is closed under language unions, which makes it interesting for practical applications. In this paper, we investigate this notion in the framework of coordination control. We prove that conditional normality is a stronger condition than conditional (strong) relative observability, hence conditional strong relative observability can be used in coordination control instead of conditional normality, and present a distributive procedure for the computation of a conditionally controllable and conditionally observable sublanguage of the specification that contains the supremal conditionally strong relative observable sublanguage. △ Less

Submitted 8 April, 2014; originally announced April 2014.

Comments: arXiv admin note: substantial text overlap with arXiv:1403.4762

Decentralized Supervisory Control with Communicating Supervisors Based on Top-Down Coordination Control

Authors: Jan Komenda, Tomáš Masopust

Abstract: In this paper we present a new approach to decentralized supervisory control of large automata with communicating supervisors. We first generalize the recently developed top-down architecture of multilevel coordination control with a hierarchical structure of groups of subsystems, their respective coordinators and supervisors. Namely, in the case where the equivalent conditions for achieving a spe… ▽ More In this paper we present a new approach to decentralized supervisory control of large automata with communicating supervisors. We first generalize the recently developed top-down architecture of multilevel coordination control with a hierarchical structure of groups of subsystems, their respective coordinators and supervisors. Namely, in the case where the equivalent conditions for achieving a specification language fail to be satisfied, we propose sufficient conditions for a distributed computation of the supremal achievable sublanguage. We then apply the obtained constructive results of multilevel coordination control to decentralized supervisory control with communication, where local supervisors of subsystems within a group communicate with each other via the coordinator of the group. Our approach is illustrated by an example. △ Less

Submitted 20 March, 2014; originally announced March 2014.

Maximally Permissive Coordination Supervisory Control -- Towards Necessary and Sufficient Conditions

Authors: Jan Komenda, Tomáš Masopust, Jan H. van Schuppen

Abstract: In this paper, we further develop the coordination control framework for discrete-event systems with both complete and partial observation. A new weaker sufficient condition for the computation of the supremal conditionally controllable sublanguage is presented. This result is then used for the computation of the supremal conditionally controllable and conditionally normal sublanguage. The paper f… ▽ More In this paper, we further develop the coordination control framework for discrete-event systems with both complete and partial observation. A new weaker sufficient condition for the computation of the supremal conditionally controllable sublanguage is presented. This result is then used for the computation of the supremal conditionally controllable and conditionally normal sublanguage. The paper further generalizes the previous study by considering general, non-prefix-closed languages. △ Less

Submitted 19 March, 2014; originally announced March 2014.

Coordination Control of Discrete-Event Systems Revisited

Authors: Jan Komenda, Tomas Masopust, Jan H. van Schuppen

Abstract: In this paper, we revise and further investigate the coordination control approach proposed for supervisory control of distributed discrete-event systems with synchronous communication based on the Ramadge-Wonham automata framework. The notions of conditional decomposability, conditional controllability, and conditional closedness ensuring the existence of a solution are carefully revised and simp… ▽ More In this paper, we revise and further investigate the coordination control approach proposed for supervisory control of distributed discrete-event systems with synchronous communication based on the Ramadge-Wonham automata framework. The notions of conditional decomposability, conditional controllability, and conditional closedness ensuring the existence of a solution are carefully revised and simplified. The paper is generalized to non-prefix-closed languages, that is, supremal conditionally controllable sublanguages of not necessary prefix-closed languages are discussed. Non-prefix-closed languages introduce the blocking issue into coordination control, hence a procedure to compute a coordinator for nonblockingness is included. The optimization problem concerning the size of a coordinator is under investigation. We prove that to find the minimal extension of the coordinator event set for which a given specification language is conditionally decomposable is NP-hard. In other words, unless P=NP, it is not possible to find a polynomial algorithm to compute the minimal coordinator with respect to the number of events. △ Less

Submitted 16 July, 2013; originally announced July 2013.

Journal ref: Discrete Event Dynamic Systems 25(1), 65-94, 2015

On the State Complexity of the Reverse of R- and J-trivial Regular Languages

Authors: Galina Jirásková, Tomáš Masopust

Abstract: The tight upper bound on the state complexity of the reverse of R-trivial and J-trivial regular languages of the state complexity n is 2^{n-1}. The witness is ternary for R-trivial regular languages and (n-1)-ary for J-trivial regular languages. In this paper, we prove that the bound can be met neither by a binary R-trivial regular language nor by a J-trivial regular language over an (n-2)-element… ▽ More The tight upper bound on the state complexity of the reverse of R-trivial and J-trivial regular languages of the state complexity n is 2^{n-1}. The witness is ternary for R-trivial regular languages and (n-1)-ary for J-trivial regular languages. In this paper, we prove that the bound can be met neither by a binary R-trivial regular language nor by a J-trivial regular language over an (n-2)-element alphabet. We provide a characterization of tight bounds for R-trivial regular languages depending on the state complexity of the language and the size of its alphabet. We show the tight bound for J-trivial regular languages over an (n-2)-element alphabet and a few tight bounds for binary J-trivial regular languages. The case of J-trivial regular languages over an (n-k)-element alphabet, for 2 <= k <= n-3, is open. △ Less

Submitted 10 June, 2013; v1 submitted 2 April, 2013; originally announced April 2013.

Comments: Full version of the paper accepted for DCFS 2013

Efficient Separability of Regular Languages by Subsequences and Suffixes

Authors: Wojciech Czerwiński, Wim Martens, Tomáš Masopust

Abstract: When can two regular word languages K and L be separated by a simple language? We investigate this question and consider separation by piecewise- and suffix-testable languages and variants thereof. We give characterizations of when two languages can be separated and present an overview of when these problems can be decided in polynomial time if K and L are given by nondeterministic automata. When can two regular word languages K and L be separated by a simple language? We investigate this question and consider separation by piecewise- and suffix-testable languages and variants thereof. We give characterizations of when two languages can be separated and present an overview of when these problems can be decided in polynomial time if K and L are given by nondeterministic automata. △ Less

Submitted 5 March, 2013; originally announced March 2013.

A Note on Limited Pushdown Alphabets in Stateless Deterministic Pushdown Automata

Authors: Tomáš Masopust

Abstract: Recently, an infinite hierarchy of languages accepted by stateless deterministic pushdown automata has been established based on the number of pushdown symbols. However, the witness language for the n-th level of the hierarchy is over an input alphabet with 2(n-1) elements. In this paper, we improve this result by showing that a binary alphabet is sufficient to establish this hierarchy. As a conse… ▽ More Recently, an infinite hierarchy of languages accepted by stateless deterministic pushdown automata has been established based on the number of pushdown symbols. However, the witness language for the n-th level of the hierarchy is over an input alphabet with 2(n-1) elements. In this paper, we improve this result by showing that a binary alphabet is sufficient to establish this hierarchy. As a consequence of our construction, we solve the open problem formulated by Meduna et al. Then we extend these results to m-state realtime deterministic pushdown automata, for all m at least 1. The existence of such a hierarchy for m-state deterministic pushdown automata is left open. △ Less

Submitted 24 August, 2012; originally announced August 2012.

MSC Class: 68Q45

On Algorithms and Extensions of Coordination Control of Discrete-Event Systems

Authors: Jan Komenda, Tomáš Masopust, Jan H. van Schuppen

Abstract: In this paper, we further develop the coordination control scheme for discrete-event systems based on the Ramadge-Wonham framework. The notions of conditional decomposability, conditional controllability, and conditional closedness are revised and simplified, supremal conditionally controllable sublanguages of general non-prefix-closed languages are discussed, and a procedure for the computation o… ▽ More In this paper, we further develop the coordination control scheme for discrete-event systems based on the Ramadge-Wonham framework. The notions of conditional decomposability, conditional controllability, and conditional closedness are revised and simplified, supremal conditionally controllable sublanguages of general non-prefix-closed languages are discussed, and a procedure for the computation of a coordinator for nonblockingness is presented. △ Less

Submitted 26 July, 2012; originally announced July 2012.

Comments: WODES 2012, Guadalajara, Mexico

A Note on Undecidability of Observation Consistency for Non-Regular Languages

Authors: Tomáš Masopust

Abstract: One of the most interesting questions concerning hierarchical control of discrete-event systems with partial observations is a condition under which the language observability is preserved between the original and the abstracted plant. Recently, we have characterized two such sufficient conditions---observation consistency and local observation consistency. In this paper, we prove that the conditi… ▽ More One of the most interesting questions concerning hierarchical control of discrete-event systems with partial observations is a condition under which the language observability is preserved between the original and the abstracted plant. Recently, we have characterized two such sufficient conditions---observation consistency and local observation consistency. In this paper, we prove that the condition of observation consistency is undecidable for non-regular (linear, deterministic context-free) languages. The question whether the condition is decidable for regular languages is open. △ Less

Submitted 9 January, 2012; originally announced January 2012.

MSC Class: 68Q45; 93C65; 93A13; 93B07

On Conditional Decomposability

Authors: Jan Komenda, Tomáš Masopust, Jan H. van Schuppen

Abstract: The requirement of a language to be conditionally decomposable is imposed on a specification language in the coordination supervisory control framework of discrete-event systems. In this paper, we present a polynomial-time algorithm for the verification whether a language is conditionally decomposable with respect to given alphabets. Moreover, we also present a polynomial-time algorithm to extend… ▽ More The requirement of a language to be conditionally decomposable is imposed on a specification language in the coordination supervisory control framework of discrete-event systems. In this paper, we present a polynomial-time algorithm for the verification whether a language is conditionally decomposable with respect to given alphabets. Moreover, we also present a polynomial-time algorithm to extend the common alphabet so that the language becomes conditionally decomposable. A relationship of conditional decomposability to nonblockingness of modular discrete-event systems is also discussed in this paper in the general settings. It is shown that conditional decomposability is a weaker condition than nonblockingness. △ Less

Submitted 19 December, 2014; v1 submitted 9 January, 2012; originally announced January 2012.

Comments: A few minor corrections

MSC Class: 93C65; 93A99; 93B50

Journal ref: Systems & Control Letters 61 (12), 1260-1268, 2012

Supervisory Control Synthesis of Discrete-Event Systems using Coordination Scheme

Authors: Jan Komenda, Tomas Masopust, Jan H. van Schuppen

Abstract: Supervisory control of discrete-event systems with a global safety specification and with only local supervisors is a difficult problem. For global specifications the equivalent conditions for local control synthesis to equal global control synthesis may not be met. This paper formulates and solves a control synthesis problem for a generator with a global specification and with a combination of a… ▽ More Supervisory control of discrete-event systems with a global safety specification and with only local supervisors is a difficult problem. For global specifications the equivalent conditions for local control synthesis to equal global control synthesis may not be met. This paper formulates and solves a control synthesis problem for a generator with a global specification and with a combination of a coordinator and local controllers. Conditional controllability is proven to be an equivalent condition for the existence of such a coordinated controller. A procedure to compute the least restrictive solution is also provided in this paper and conditions are stated under which the result of our procedure coincides with the supremal controllable sublanguage. △ Less

Submitted 16 July, 2010; originally announced July 2010.

Comments: 29 pages, 11 figures

Comparison of Two Context-Free Rewriting Systems with Simple Context-Checking Mechanisms

Authors: Tomas Masopust

Abstract: This paper solves an open problem concerning the generative power of nonerasing context-free rewriting systems using a simple mechanism for checking for context dependencies, in the literature known as semi-conditional grammars of degree (1,1). In these grammars, two nonterminal symbols are attached to each context-free production, and such a production is applicable if one of the two attached sym… ▽ More This paper solves an open problem concerning the generative power of nonerasing context-free rewriting systems using a simple mechanism for checking for context dependencies, in the literature known as semi-conditional grammars of degree (1,1). In these grammars, two nonterminal symbols are attached to each context-free production, and such a production is applicable if one of the two attached symbols occurs in the current sentential form, while the other does not. Specifically, this paper demonstrates that the family of languages generated by semi-conditional grammars of degree (1,1) coincides with the family of random context languages. In addition, it shows that the normal form proved by Mayer for random context grammars with erasing productions holds for random context grammars without erasing productions, too. It also discusses two possible definitions of the relation of the direct derivation step used in the literature. △ Less

Submitted 21 April, 2010; originally announced April 2010.

Comments: Unpublished as a stronger result is under consideration.

MSC Class: 68Q42; 68Q45

Descriptional Complexity of Three-Nonterminal Scattered Context Grammars: An Improvement

Authors: Tomáš Masopust, Alexander Meduna

Abstract: Recently, it has been shown that every recursively enumerable language can be generated by a scattered context grammar with no more than three nonterminals. However, in that construction, the maximal number of nonterminals simultaneously rewritten during a derivation step depends on many factors, such as the cardinality of the alphabet of the generated language and the structure of the generated… ▽ More Recently, it has been shown that every recursively enumerable language can be generated by a scattered context grammar with no more than three nonterminals. However, in that construction, the maximal number of nonterminals simultaneously rewritten during a derivation step depends on many factors, such as the cardinality of the alphabet of the generated language and the structure of the generated language itself. This paper improves the result by showing that the maximal number of nonterminals simultaneously rewritten during any derivation step can be limited by a small constant regardless of other factors. △ Less

Submitted 29 July, 2009; originally announced July 2009.

Journal ref: EPTCS 3, 2009, pp. 183-192

Answers to Questions Formulated in the Paper "On States Observability in Deterministic Finite Automata"

Authors: Tomas Masopust

Abstract: This paper gives answers to questions formulated as open in the paper "On State Observability in Deterministic Finite Automata" by A. Mateescu and Gh. Paun. Specifically, it demonstrates that for all k >= 2, the families of regular languages acceptable by deterministic finite automata with no more than k semi-observable states, denoted by Tk, are anti-AFL's, and that the family T1 differs in the… ▽ More This paper gives answers to questions formulated as open in the paper "On State Observability in Deterministic Finite Automata" by A. Mateescu and Gh. Paun. Specifically, it demonstrates that for all k >= 2, the families of regular languages acceptable by deterministic finite automata with no more than k semi-observable states, denoted by Tk, are anti-AFL's, and that the family T1 differs in the closure property under Kleene +. △ Less

Submitted 26 May, 2009; originally announced May 2009.

ACM Class: F.4.3