Wyniki wyszukiwania - Biblioteka Nauki

1

On Languages of P Automata

100%

Csuhaj-Varjú E. , Vaszil G.

Fundamenta Informaticae

|

2020

|

tom Vol. 171, nr 1-4

133--149

EN

P automata are accepting computing devices combining features of classical automata and membrane systems. In this paper we introduce P n-stack-automata, a restricted class of P automata that mimics the behaviour of n-stack automata. We show that for n = 1 these constructs describe the context-free language class and for n = 3 the class of quasi-realtime languages.

2

SAT-based Reachability Checking for Timed Automata with Diagonal Constraints

80%

Zbrzezny A.

Fundamenta Informaticae

|

2005

|

tom Vol. 67, nr 1-3

303--322

EN

This paper deals with the problem of checking reachability for timed automata with diagonal constraints. Such automata are needed in many applications e.g. to model scheduling problems. We introduce a new discretization for timed automata which enables SAT based reachability analysis for timed automata for which comparisons between two clocks are allowed. In our earlier papers SAT based reachability analysis was restricted to the so called diagonal-free timed automata, where only comparisons between clocks and constants are allowed.

3

Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction

80%

Cassez F. , Jensen P. G. , Guldstrand Larsen K.

Fundamenta Informaticae

|

2021

|

tom Vol. 178, nr 1/2

31--57

EN

We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. We propose a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs. All of the algorithms proposed have been implemented and we have conducted a series of experiments, comparing the performance of our new approach to state-of-the-art tools in classical reachability, robustness analysis and parameter synthesis for timed systems. We show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.

4

Improvements in SAT-based Reachability Analysis for Timed Automata

80%

Zbrzezny A.

Fundamenta Informaticae

|

2004

|

tom Vol. 60, nr 1-4

417--434

EN

The paper deals with the problem of checking reachability for timed automata. In order to check reachability of a state satisfying some property, first the transition relation of a timed automaton is unfolded iteratively to some depth and encoded as a propositional formula. Next, the property is translated to a propositional formula and satisfiability of the conjunction of the two defined above formulas is checked. The unfolding of the transition relation can be terminated when either a state satisfying the property has been found or all the states of the timed automaton have been searched. In this paper we propose some improvements of the encoding of the transition relation for timed automata. The improvements are partially based on a new discretization scheme. The efficiency of the improved encoding is strongly supported by the experimental results. We also introduce a method for checking unreachability.

5

It is Undecidable if Two Regular Tree Languages can be Separated by a Deterministic Tree-walking Automaton

70%

Bojańczyk M.

Fundamenta Informaticae

|

2017

|

tom Vol. 154, nr 1/4

37--46

EN

The following problem is shown undecidable: given regular languages L, K of finite trees, decide if there exists a deterministic tree-walking automaton which accepts all trees in L and rejects all trees in K. The proof uses a technique of Kopczyński from [1].

6

A Sweep-Line Method for Büchi Automata-based Model Checking

70%

Evangelista S. , Kristensen L. M.

Fundamenta Informaticae

|

2014

|

tom Vol. 131, nr 1

27--53

EN

The sweep-line method allows explicit state model checkers to delete states from memory on-the-fly during state space exploration, thereby lowering the memory demands of the verification procedure. The sweep-line method is based on a least-progress-first search order that prohibits the immediate use of standard on-the-fly Büchi automata-based model checking algorithms that rely on a depth-first search order in the search for an acceptance cycle. This paper proposes and experimentally evaluates an algorithm for Büchi automata-based model checking compatible with the search order and deletion of states prescribed by the sweep-line method.

7

On Tight Separation for Blum Measures Applied to Turing Machine Buffer Complexity

70%

Šíma J. , Žák S.

Fundamenta Informaticae

|

2017

|

tom Vol. 152, nr 4

397--409

EN

We formulate a very general tight diagonalization method for the Blum complexity measures satisfying two additional axioms related to our diagonalizer machine. We apply this method to two new, mutually related, distance and buffer complexities of Turing machine computations which are important nontrivial examples of natural Blum complexity measures different from time and space. In particular, these measures capture how many times the worktape head needs to move a certain distance during the computation which corresponds to the number of necessary block uploads into a buffer cache memory. We start this study by proving a tight separation which shows that a very small increase in the distance or buffer complexity bound (roughly from f(n) to f(n + 1)) brings provably more computational power to both deterministic and nondeterministic Turing machines even for unary languages. We also obtain hierarchies of the distance and buffer complexity classes.

8

Catalytic and Purely Catalytic P Systems and P Automata: Control Mechanisms for Obtaining Computational Completeness

70%

Freund R. , Oswald M. , Păun G.

Fundamenta Informaticae

|

2015

|

tom Vol. 136, nr 1/2

59--84

EN

The questions whether catalytic P systems with only one catalyst and purely catalytic P systems with only two catalysts can already be computationally complete in the generative case, still are open problems. For accepting P systems or P automata, the situation is even more complicated when we consider sets of vectors of natural numbers and not only sets of natural numbers – the number of catalysts increases with the dimension of the vectors. We here establish computational completeness for catalytic P systems and P automata with only one catalyst as well as for purely catalytic P systems and P automata with only two catalysts in the skin membrane by using specific variants of additional control mechanisms: in P systems and P automata with label selection, we only use rules from one set of a finite number of sets of rules in each computation step; in time-varying P systems and P automata the available sets of rules change periodically with time. The same control mechanisms also allow for computing partial recursive relations or functions of (vectors of) natural numbers when being used in catalytic P systems with one catalyst and purely catalytic P systems with two catalysts. Finally, these variants of P systems can also be used to generate or accept strings and to compute partial relations or functions on strings, and again we obtain computational completeness with only one catalyst in the case of catalytic P systems and two catalysts in the case of purely catalytic P systems.

9

Deterministic One-Way Turing Machines with Sublinear Space

70%

Kutrib M. , Provillard J. , Vaszil G. , Wendlandt M.

Fundamenta Informaticae

|

2015

|

tom Vol. 136, nr 1/2

139--155

EN

Deterministic one-way Turing machines with sublinear space bounds are systematically studied. We distinguish among the notions of strong, weak, and restricted space bounds. The latter is motivated by the study of P automata. The space available on the work tape depends on the number of input symbols read so far, instead of the entire input. The class of functions space constructible by such machines is investigated, and it is shown that every function f that is space constructible by a deterministic two-way Turing machine, is space constructible by a strongly f space-bounded deterministic one-way Turing machine as well. We prove that the restricted mode coincides with the strong mode for space constructible functions. The known infinite, dense, and strict hierarchy of strong space complexity classes is derived also for the weak mode by Kolmogorov complexity arguments. Finally, closure properties under AFL operations, Boolean operations and reversal are shown.

10

The Supports of Weighted Unranked Tree Automata

70%

Droste M. , Heusel D.

Fundamenta Informaticae

|

2015

|

tom Vol. 136, nr 1/2

37--58

EN

We investigate the supports of weighted unranked tree automata. Our main result states that the support of a weighted unranked tree automaton over a zero-sum free, commutative strong bimonoid is recognizable. For this, we use methods of Kirsten (DLT 2009), in particular, his construction of finite automata recognizing the supports of weighted automata on strings over zero-sum free, commutative semirings. We also get an effective construction of a finite tree automaton recognizing the support of a given weighted unranked tree automaton for zero-sum free, commutative strong bimonoids where Kirsten’s zero generation problem is decidable. In addition, we give a translation of nested weighted automata into weighted unranked tree automata for arbitrary commutative strong bimonoids. As a consequence,we derive analogous results for the supports of nested weighted automata. Finally, we give similar results for the supports of weighted pushdown automata.

11

The Number of Distinct Subpalindromes in Random Words

70%

Rubinchik M. , Shur A. M.

Fundamenta Informaticae

|

2016

|

tom Vol. 145, nr 3

371--384

EN

We prove that a random word of length n over a k-ary fixed alphabet contains, on expectation,Θ(√n) distinct palindromic factors. We study this number of factors, E(n, k), in detail, showing that the limit limn→∞ E(n, k)=√n does not exist for any κ ≥ 2, lim infn→∞ E(n; k)=√n =Θ(1), and lim supn→∞ E(n; k)=√n = Θ(√k). Such a complicated behaviour stems from the asymmetry between the palindromes of even and odd length. We show that a similar, but much simpler, result on the expected number of squares in random words holds. We also provide some experimental data on the number of palindromic factors in random words.

12

Twelve Years of QBF Evaluations : QSAT Is PSPACE-Hard and It Shows

70%

Marin P. , Pulina L. , Giunchiglia E. , Narizzano M. , Tacchella A.

Fundamenta Informaticae

|

2016

|

tom Vol. 149, nr 1/2

133--158

EN

Twelve years have elapsed since the first Quantified Boolean Formulas (QBFs) evaluation was held as an event linked to SAT conferences. During this period, researchers have striven to propose new algorithms and tools to solve challenging formulas, with evaluations periodically trying to assess the current state of the art. In this paper, we present an experimental account of solvers and formulas with the aim to understand the progress in the QBF arena across these years. Unlike typical evaluations, the analysis is not confined to the snapshot of submitted solvers and formulas, but rather we consider several tools that were proposed over the last decade, and we run them on different formulas from previous QBF evaluations. The main contributions of our analysis, which are also the messages we would like to pass along to the research community, are: (i) many formulas that turned out to be difficult to solve in past evaluations, remain still challenging after twelve years, (ii) there is no single solver which can significantly outperform all the others, unless specific categories of formulas are considered, and (iii) effectiveness of preprocessing depends both on the coupled solver and the structure of the formula.

13

A Nonarchimedian Discretization for Timed Languages

70%

Dima C.

Fundamenta Informaticae

|

2014

|

tom Vol. 131, nr 3-4

389--407

EN

We give a discretization of behaviors of timed automata, in which timed languages are represented as sets of words containing action symbols, a clock tick symbol 1, and two delay symbols δ− (negative delay) and δ+ (positive delay). Unlike the region construction, our discretization commutes with intersection. We show that discretizations of timed automata are, in general, context-sensitive languages over Σ ∪ {1, δ+, δ−}, and give a class of counter automata that accepts exactly the class of languages that are discretizations of timed automata, and show that its emptiness problem is decidable.

14

Power of S-kR-RRWW-automata

70%

Hoffmann P.

Fundamenta Informaticae

|

2015

|

tom Vol. 136, nr 1/2

85--112

EN

Single k-reversible restarting automata are a special version of restarting automata which can be effectively learned from samples. We show that their power lies between GCSL and CSL. We show that their subclasses form an infinite hierarchy of classes of languages with respect to the reversibility level k and we also show that limiting types of allowed rewrites lowers the power of the model. Finally, we study their relation to strictly locally testable restarting automata.

15

On the Computational Complexity of Partial Word Automata Problems

70%

Holzer M. , Jakobi S. , Wendlandt M.

Fundamenta Informaticae

|

2016

|

tom Vol. 148, nr 3/4

267--289

EN

We consider the computational complexity of problems related to partial word automata. Roughly speaking, a partial word is a word in which some positions are unspecified and a partial word automaton is a finite automaton that accepts a partial word language-here the unspecified positions in the word are represented by a "hole" symbol ◊ . A partial word language L' can be transformed into an ordinary language L by using a ◊-substitution. In particular, we investigate the complexity of the compression or minimization problem for partial word automata, which is known to be NP-hard. We improve on the previously known complexity on this problem, by showing PSPACE-completeness. In fact, it turns out that almost all problems related to partial word automata, such as, e.g., equivalence and universality, are already PSPACE- complete. Moreover, we also study these problems under the further restriction that the involved automata accept only finite languages. In this case, the complexities of the studied problems drop from PSPACE-completeness down to coNP-hardness and containment in ∑P2 depending on the problem investigated.

16

Reversible Queue Automata

70%

Kutrib M. , Malcher A. , Wendlandt M.

Fundamenta Informaticae

|

2016

|

tom Vol. 148, nr 3/4

341--368

EN

Deterministic finite automata equipped with the storage medium of a queue are investigated towards their ability to perform reversible computations, that is, computations in which every occurring configuration has exactly one successor and exactly one predecessor. A first result is that any queue automaton can be simulated by a reversible one. So, reversible queue automata are as powerful as Turing machines. Therefore it is of natural interest to impose time restrictions to queue automata. Here we consider quasi realtime and realtime computations. It is shown that every reversible quasi realtime queue automaton can be sped up to realtime. On the other hand, under realtime conditions reversible queue automata are less powerful than general queue automata. Furthermore, we exhibit a lower bound of ...[formula] time steps for realtime queue automata witness languages to be accepted by any equivalent reversible queue automaton. We study the closure properties of reversible realtime queue automata and obtain similar results as for reversible deterministic pushdown automata. Finally, we investigate decidability questions and obtain that all commonly studied questions such as emptiness, finiteness, or equivalence are not semidecidable for reversible realtime queue automata. Furthermore, it is not semidecidable whether an arbitrary given realtime queue automaton is reversible.

17

Adding Data Registers to Parameterized Networks with Broadcast

70%

Delzanno G. , Sangnier A. , Traverso R.

Fundamenta Informaticae

|

2016

|

tom Vol. 143, nr 3/4

287--316

EN

We study parameterized verification problems for networks of interacting register automata. The network is represented through a graph, and processes may exchange broadcast messages containing data with their neighbours. Upon reception a process can either ignore a sent value, test for equality with a value stored in a register, or simply store the value in a register. We consider safety properties expressed in terms of reachability, from arbitrarily large initial configurations, of a configuration exposing some given control states and patterns. We investigate, in this context, the impact on decidability and complexity of the number of local registers, the number of values carried by a single message, and dynamic reconfigurations of the underlying network.

18

Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking

70%

Woźna-Szcześniak B. , Zbrzezny A.

Fundamenta Informaticae

|

2014

|

tom Vol. 135, nr 4

553--568

EN

We investigate a SAT-based bounded model checking (BMC) method for MTL (metric temporal logic) that is interpreted over linear discrete infinite time models generated by discrete timed automata. In particular, we translate the existential model checking problem for MTL to the existential model checking problem for a variant of linear temporal logic (called HLTL), and we provide a SAT-based BMC technique for HLTL. We show how to implement the BMC technique for HLTL and discrete timed automata, and as a case study we apply the technique in the analysis of GTPP, a Generic Timed Pipeline Paradigm modelled by a network of discrete timed automata.

19

Variants of Small Universal P Systems with Catalysts

70%

Alhazov A. , Freund R.

Fundamenta Informaticae

|

2015

|

tom Vol. 138, nr 1/2

227--250

EN

Computational completeness is known for P systems with two catalysts and purely catalytic P systems with three catalysts as well as for P systems with one bi-stable catalyst. We complete this picture by showing computational completeness for purely catalytic P systems with one bi-stable catalyst and one catalyst. Moreover, we present some concrete universal P systems, e.g., for P systems with one multi-stable catalyst and for P systems with multiple catalysts. Furthermore, we optimize the descriptional complexity of Minsky’s reduction from register machines with an arbitrary number of registers to register machines with only two registers. In that way, we are able to transformthe universalmachines U22 and U20 of Korec into weakly universal register machines with only two decrementable registers, one even with unencoded output. Based on these universal register machines, we then construct small universal P systems with one bi-stable catalyst and one catalyst as well as small universal purely catalytic P systems with three catalysts. With respect to the number of rules, the smallest universal P systems can be obtained with multi-stable catalysts and with multiple catalysts. The number of rules in all these systems can be further reduced by adding the concept of toxic objects (a specified subset of objects), where all computation branches not evolving all toxic objects in every computation step do not yield a result.

20

Interrupt Timed Automata with Auxiliary Clocks and Parameters

70%

Bérard B. , Jovanović A. , Haddad S. , Lime D.

Fundamenta Informaticae

|

2016

|

tom Vol. 143, nr 3/4

235--259

EN

Interrupt Timed Automata (ITA) are an expressive timed model, introduced to take into account interruptions according to levels. Due to this feature, this formalism is incomparable with Timed Automata. However several decidability results related to reachability and model checking have been obtained. We add auxiliary clocks to ITA, thereby extending its expressive power while preserving decidability of reachability. Moreover, we define a parametrized version of ITA, with polynomials of parameters appearing in guards and updates. While parametric reasoning is particularly relevant for timed models, it very often leads to undecidability results. We prove that various reachability problems, including robust reachability, are decidable for this model, and we give complexity upper bounds for a fixed or variable number of clocks, levels and parameters.