Improvement in JavaMOP by Simplifying Büchi Automaton

2018 ◽  
pp. 129-134
Author(s):  
Junyan Qian ◽  
Cong Chen ◽  
Wei Cao ◽  
Zhongyi Zhai ◽  
Lingzhong Zhao
Keyword(s):  
Büchi Automaton

scholarly journals FACTORIZATIONS AND UNIVERSAL AUTOMATON OF OMEGA LANGUAGES

2014 ◽  
Vol 25 (08) ◽  
pp. 1111-1125
Author(s):  
VINCENT CARNINO ◽  
SYLVAIN LOMBARDY
Keyword(s):  
Normal Form ◽  
Büchi Automata ◽  
Morphic Image ◽  
Rational Language ◽  
Büchi Automaton ◽  
Buchi Automata

We extend the concept of factorization on finite words to ω-rational languages and show how to compute them. We define a normal form for Büchi automata and introduce a universal automaton for Büchi automata in normal form. We prove that, for every ω-rational language, this Büchi automaton, based on factorization, is canonical and that it is the smallest automaton that contains the morphic image of every equivalent Büchi automaton in normal form.

scholarly journals Is there a best büchi automaton for explicit model checking?

2014 ◽  
Author(s):  
František Blahoudek ◽  
Alexandre Duret-Lutz ◽  
Mojmír Křetínský ◽  
Jan Strejček
Keyword(s):  
Model Checking ◽  
Explicit Model ◽  
Büchi Automaton

A Framework-Driven Comparison of Automata-Based Tools for Identifying Business Rule Conflicts

2019 ◽  
Vol 29 (03) ◽  
pp. 433-455
Author(s):  
Vitus S. W. Lam
Keyword(s):  
Temporal Logic ◽  
Linear Temporal Logic ◽  
Process Models ◽  
Business Rules ◽  
Business Rule ◽  
Business Process Models ◽  
Formal Framework ◽  
Automated Tools ◽  
Büchi Automaton

Drawing on business rules for constructing business process models by a constraint-driven methodology is a distinct characteristic of declarative process modeling. Given the intricacies of business rules, there is a pragmatic need to conduct conflict-free assessments for business rules in an automatic manner. In this paper, business rules are stated in terms of restricted English by harnessing a group of predefined business rule templates. With linear temporal logic that serves as a semantic foundation for the business rule templates, a pair of business rules represented as a linear temporal logic specification is translated into an associated Büchi automaton via LTL2BA, LTL3BA and ltl2tgba. A Büchi automaton that accepts the empty language signifies that the two business rules are in conflict with each other. The suitability of the formal framework and the three automated tools is evaluated by an industry-level case study.

THE EFFECT OF THE NUMBER OF SUCCESSFUL PATHS IN A BÜCHI TREE AUTOMATON

1993 ◽  
Vol 03 (02) ◽  
pp. 237-250
Author(s):  
D. BEAUQUIER ◽  
M. NIVAT ◽  
D. NIWIŃSKI
Keyword(s):  
Cardinal Number ◽  
Tree Automaton ◽  
Büchi Automata ◽  
Infinite Trees ◽  
Acceptance Condition ◽  
Tree Languages ◽  
Büchi Automaton ◽  
Buchi Automata ◽  
Computation Path

We modify an acceptance condition of Büchi automaton on infinite trees: rather than to require that each computation path is successful, we impose various restrictions on the number of successful paths in a run of the automaton on a tree. All these modifications alter the recognizing power of Büchi automata. We examine the classes induced by the acceptance conditions that require ≤α, ≥α, =α successful paths, where α is a cardinal number. It turns out that, except for some trivial cases, the “≤” classes are incomparable with the class Bü of Büchi acceptable tree languages, while the classes “≥” are strictly included in Bü.

scholarly journals COMPUTABLE SEMANTICS FOR CTL* ON DISCRETE-TIME AND CONTINUOUS-SPACE DYNAMIC SYSTEMS

2011 ◽  
Vol 22 (04) ◽  
pp. 801-821
Author(s):  
PIETER COLLINS ◽  
IVAN S. ZAPREEV
Keyword(s):  
Model Checking ◽  
Discrete Time ◽  
Dynamic Systems ◽  
Parallel Composition ◽  
Computable Model ◽  
Continuous Space ◽  
Büchi Automaton

In this work, we consider Discrete-Time Continuous-Space Dynamic Systems for which we study the computability of the standard semantics of CTL* (CTL, LTL) and provide a variant thereof computable in the sense of Type-2 Theory of Effectivity. In particular, we show how the computable model checking of existentially and universally quantified path formulae of LTL can be reduced to solving, respectively, repeated reachability and persistence problems on a model obtained as a parallel composition of the original one and a non-deterministic Büchi automaton corresponding to the verified LTL formula.

The complexity of weakly recognizing morphisms

2018 ◽  
Vol 53 (1-2) ◽  
pp. 1-17
Author(s):  
Lukas Fleischer ◽  
Manfred Kufleitner
Keyword(s):  
Computational Complexity ◽  
Regular Languages ◽  
Decision Problems ◽  
Membership Problem ◽  
Surjective Morphism ◽  
Infinite Words ◽  
Descriptional Complexity ◽  
Emptiness Problem ◽  
Free Semigroups ◽  
Büchi Automaton

Weakly recognizing morphisms from free semigroups onto finite semigroups are a classical way for defining the class of ω-regular languages, i.e., a set of infinite words is weakly recognizable by such a morphism if and only if it is accepted by some Büchi automaton. We study the descriptional complexity of various constructions and the computational complexity of various decision problems for weakly recognizing morphisms. The constructions we consider are the conversion from and to Büchi automata, the conversion into strongly recognizing morphisms, as well as complementation. We also show that the fixed membership problem is NC1-complete, the general membership problem is in L and that the inclusion, equivalence and universality problems are NL-complete. The emptiness problem is shown to be NL-complete if the input is given as a non-surjective morphism.

Model Checking of Constraint-Based Workflow Based on Linear Temporal Logic

2012 ◽  
Vol 601 ◽  
pp. 401-405
Author(s):  
Wen Bo Zhou ◽  
Shu Zhen Yao
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Business Processes ◽  
Workflow Management ◽  
Linear Temporal Logic ◽  
Management Systems ◽  
Workflow Management Systems ◽  
Model Based ◽  
Büchi Automaton ◽  
Constraint Based Models

The degree of flexibility of workflow management systems heavily influences the way business processes are executed. Constraint-based models are considered to be more flexible than traditional models because of their semantics: everything that does not violate constraints is allowed. More and more people use declarative languages to define workflow, such as linear temporal logic. But how to guarantee the correctness of the model based on the linear temporal logic is still a problem. This article proposes a way to verify the model based on Büchi automaton and gives the corresponding algorithms. Thus the verification of declarative workflow based on the linear temporal logic is solved.

scholarly journals Two Effective Properties of ω-Rational Functions

2021 ◽  
pp. 1-20
Author(s):  
Olivier Finkel
Keyword(s):  
Effective Properties ◽  
Rational Functions ◽  
Baire Class ◽  
Infinite Words ◽  
Finite State ◽  
First Baire Class ◽  
Büchi Automaton

We prove two new effective properties of rational functions over infinite words which are realized by finite state Büchi transducers. Firstly, for each such function [Formula: see text], one can construct a deterministic Büchi automaton [Formula: see text] accepting a dense [Formula: see text]-subset of [Formula: see text] such that the restriction of [Formula: see text] to [Formula: see text] is continuous. Secondly, we give a new proof of the decidability of the first Baire class for synchronous [Formula: see text]-rational functions from which we get an extension of this result involving the notion of Wadge classes of regular [Formula: see text]-languages.

scholarly journals The Determinacy of Context-Free Games

2013 ◽  
Vol 78 (4) ◽  
pp. 1115-1134 ◽  
Author(s):  
Olivier Finkel
Keyword(s):  
Set Theory ◽  
Winning Strategy ◽  
Large Cardinal ◽  
Büchi Automata ◽  
Büchi Automaton ◽  
Buchi Automata ◽  
Context Free

AbstractWe prove that the determinacy of Gale-Stewart games whose winning sets are accepted by realtime 1-counter Büchi automata is equivalent to the determinacy of (effective) analytic Gale-Stewart games which is known to be a large cardinal assumption. We show also that the determinacy of Wadge games between two players in charge ofω-languages accepted by 1-counter Büchi automata is equivalent to the (effective) analytic Wadge determinacy. Using some results of set theory we prove that one can effectively construct a 1-counter Büchi automatonand a Büchi automatonsuch that: (1) There exists a model of ZFC in which Player 2 has a winning strategy in the Wadge gameW(L(),L()); (2) There exists a model of ZFC in which the Wadge gameW(L(),L()) is not determined. Moreover these are the only two possibilities, i.e. there are no models of ZFC in which Player 1 has a winning strategy in the Wadge gameW(L(),L()).

Sign in / Sign up

Export Citation Format

Share Document