Journal articles on the topic 'Omega-Regular languages'
To see the other types of publications on this topic, follow the link: Omega-Regular languages.
Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles
Consult the top 16 journal articles for your research on the topic 'Omega-Regular languages.'
Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.
You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.
Browse journal articles on a wide variety of disciplines and organise your bibliography correctly.
1
Angluin, Dana, and Dana Fisman. "Learning regular omega languages." Theoretical Computer Science 650 (October 2016): 57–72. http://dx.doi.org/10.1016/j.tcs.2016.07.031.
Full text
2
Angluin, Dana, and Dana Fisman. "Regular omega-Languages with an Informative Right Congruence." Electronic Proceedings in Theoretical Computer Science 277 (September 7, 2018): 265–79. http://dx.doi.org/10.4204/eptcs.277.19.
Full text
3
Falah, Amin, Shibashis Guha, and Ashutosh Trivedi. "Reinforcement Learning for Omega-Regular Specifications on Continuous-Time MDP." Proceedings of the International Conference on Automated Planning and Scheduling 33, no. 1 (July 1, 2023): 578–86. http://dx.doi.org/10.1609/icaps.v33i1.27239.
Full textAbstract:
Continuous-time Markov decision processes (CTMDPs) are canonical models to express sequential decision-making under dense-time and stochastic environments. When the stochastic evolution of the environment is only available via sampling, model-free reinforcement learning (RL) is the algorithm-of-choice to compute optimal decision sequence. RL, on the other hand, requires the learning objective to be encoded as scalar reward signals. Since doing such translations manually is both tedious and error-prone, a number of techniques have been proposed to translate high-level objectives (expressed in logic or automata formalism) to scalar rewards for discrete-time Markov decision processes. Unfortunately, no automatic translation exists for CTMDPs. We consider CTMDP environments against the learning objectives expressed as omega-regular languages. Omega-regular languages generalize regular languages to infinite-horizon specifications and can express properties given in popular linear-time logic LTL. To accommodate the dense-time nature of CTMDPs, we consider two different semantics of omega-regular objectives: 1) satisfaction semantics where the goal of the learner is to maximize the probability of spending positive time in the good states, and 2) expectation semantics where the goal of the learner is to optimize the long-run expected average time spent in the ''good states'' of the automaton. We present an approach enabling correct translation to scalar reward signals that can be readily used by off-the-shelf RL algorithms for CTMDPs. We demonstrate the effectiveness of the proposed algorithms by evaluating it on some popular CTMDP benchmarks with omega-regular objectives.
4
Almeida, J., J. C. Costa, and M. Zeitoun. "McCammond’s normal forms for free aperiodic semigroups revisited." LMS Journal of Computation and Mathematics 18, no. 1 (2015): 130–47. http://dx.doi.org/10.1112/s1461157014000448.
Full textAbstract:
AbstractThis paper revisits the solution of the word problem for ${\it\omega}$-terms interpreted over finite aperiodic semigroups, obtained by J. McCammond. The original proof of correctness of McCammond’s algorithm, based on normal forms for such terms, uses McCammond’s solution of the word problem for certain Burnside semigroups. In this paper, we establish a new, simpler, correctness proof of McCammond’s algorithm, based on properties of certain regular languages associated with the normal forms. This method leads to new applications.
5
Gnatenko, Anton Romanovich, and Vladimir Anatolyevich Zakharov. "On the Model Checking Problem for Some Extension of CTL*." Modeling and Analysis of Information Systems 27, no. 4 (December 20, 2020): 428–41. http://dx.doi.org/10.18255/1818-1015-2020-4-428-441.
Full textAbstract:
Sequential reactive systems include programs and devices that work with two streams of data and convert input streams of data into output streams. Such information processing systems include controllers, device drivers, computer interpreters. The result of the operation of such computing systems are infinite sequences of pairs of events of the request-response type, and, therefore, finite transducers are most often used as formal models for them. The behavior of transducers is represented by binary relations on infinite sequences, and so, traditional applied temporal logics (like HML, LTL, CTL, mu-calculus) are poorly suited as specification languages, since omega-languages, not binary relations on omega-words are used for interpretation of their formulae. To provide temporal logics with the ability to define properties of transformations that characterize the behavior ofreactive systems, we introduced new extensions ofthese logics, which have two distinctive features: 1) temporal operators are parameterized, and languages in the input alphabet oftransducers are used as parameters; 2) languages in the output alphabet oftransducers are used as basic predicates. Previously, we studied the expressive power ofnew extensions Reg-LTL and Reg-CTL ofthe well-known temporal logics oflinear and branching time LTL and CTL, in which it was allowed to use only regular languages for parameterization of temporal operators and basic predicates. We discovered that such a parameterization increases the expressive capabilities oftemporal logic, but preserves the decidability of the model checking problem. For the logics mentioned above, we have developed algorithms for the verification of finite transducers. At the next stage of our research on the new extensions of temporal logic designed for the specification and verification of sequential reactive systems, we studied the verification problem for these systems using the temporal logic Reg-CTL*, which is an extension ofthe Generalized Computational Tree Logics CTL*. In this paper we present an algorithm for checking the satisfiability of Reg-CTL* formulae on models of finite state transducers and show that this problem belongs to the complexity class ExpSpace.
6
CURRIE, JAMES D., NARAD RAMPERSAD, and KALLE SAARI. "Suffix conjugates for a class of morphic subshifts." Ergodic Theory and Dynamical Systems 35, no. 6 (June 4, 2014): 1767–82. http://dx.doi.org/10.1017/etds.2014.5.
Full textAbstract:
Let $A$ be a finite alphabet and $f:~A^{\ast }\rightarrow A^{\ast }$ be a morphism with an iterative fixed point $f^{{\it\omega}}({\it\alpha})$, where ${\it\alpha}\in A$. Consider the subshift $({\mathcal{X}},T)$, where ${\mathcal{X}}$ is the shift orbit closure of $f^{{\it\omega}}({\it\alpha})$ and $T:~{\mathcal{X}}\rightarrow {\mathcal{X}}$ is the shift map. Let $S$ be a finite alphabet that is in bijective correspondence via a mapping $c$ with the set of non-empty suffixes of the images $f(a)$ for $a\in A$. Let ${\mathcal{S}}\subset S^{\mathbb{N}}$ be the set of infinite words $\mathbf{s}=(s_{n})_{n\geq 0}$ such that ${\it\pi}(\mathbf{s}):=c(s_{0})f(c(s_{1}))f^{2}(c(s_{2}))\cdots \in {\mathcal{X}}$. We show that if $f$ is primitive, $f^{{\it\omega}}({\it\alpha})$ is aperiodic, and $f(A)$ is a suffix code, then there exists a mapping $H:~{\mathcal{S}}\rightarrow {\mathcal{S}}$ such that $({\mathcal{S}},H)$ is a topological dynamical system and ${\it\pi}:~({\mathcal{S}},H)\rightarrow ({\mathcal{X}},T)$ is a conjugacy; we call $({\mathcal{S}},H)$ the suffix conjugate of $({\mathcal{X}},T)$. In the special case where $f$ is the Fibonacci or Thue–Morse morphism, we show that the subshift $({\mathcal{S}},T)$ is sofic, that is, the language of ${\mathcal{S}}$ is regular.
7
Huy, Phan Trung, and Nguyễn Quý Khang. "Regular omega-languages and finite monoids having infinite products." Journal of Computer Science and Cybernetics 19, no. 2 (July 26, 2012). http://dx.doi.org/10.15625/1813-9663/19/2/1512.
Full text
8
Rabinovich, Alexander, and Doron Tiferet. "Ambiguity Hierarchy of Regular Infinite Tree Languages." Logical Methods in Computer Science Volume 17, Issue 3 (August 13, 2021). http://dx.doi.org/10.46298/lmcs-17(3:18)2021.
Full textAbstract:
An automaton is unambiguous if for every input it has at most one accepting computation. An automaton is k-ambiguous (for k > 0) if for every input it has at most k accepting computations. An automaton is boundedly ambiguous if it is k-ambiguous for some $k \in \mathbb{N}$. An automaton is finitely (respectively, countably) ambiguous if for every input it has at most finitely (respectively, countably) many accepting computations. The degree of ambiguity of a regular language is defined in a natural way. A language is k-ambiguous (respectively, boundedly, finitely, countably ambiguous) if it is accepted by a k-ambiguous (respectively, boundedly, finitely, countably ambiguous) automaton. Over finite words every regular language is accepted by a deterministic automaton. Over finite trees every regular language is accepted by an unambiguous automaton. Over $\omega$-words every regular language is accepted by an unambiguous B\"uchi automaton and by a deterministic parity automaton. Over infinite trees Carayol et al. showed that there are ambiguous languages. We show that over infinite trees there is a hierarchy of degrees of ambiguity: For every k > 1 there are k-ambiguous languages that are not k - 1 ambiguous; and there are finitely (respectively countably, uncountably) ambiguous languages that are not boundedly (respectively finitely, countably) ambiguous.
9
Klarlund, Nils, Madhavan Mukund, and Milind Sohoni. "Determinizing Asynchronous Automata on Infinite Inputs." BRICS Report Series 2, no. 58 (November 28, 1995). http://dx.doi.org/10.7146/brics.v2i58.19959.
Full textAbstract:
Asynchronous automata are a natural distributed machine model<br />for recognizing trace languages - languages defined over an alphabet<br />equipped with an independence relation.<br />To handle infinite traces, Gastin and Petit introduced Buchi asynchronous<br />automata, which accept precisely the class of omega-regular trace<br />languages. Like their sequential counterparts, these automata need to<br />be non-deterministic in order to capture all omega-regular languages. Thus<br />complementation of these automata is non-trivial. Complementation<br />is an important operation because it is fundamental for treating the<br />logical connective "not" in decision procedures for monadic second-order<br />logics. Subsequently, Diekert and Muscholl solved the complementation<br />problem by showing that with a Muller acceptance condition, deterministic<br />automata suffice for recognizing omega-regular trace languages.<br />However, a direct determinization procedure, extending the classical<br />subset construction, has proved elusive.<br />In this paper, we present a direct determinization procedure for<br />Buchi asynchronous automata, which generalizes Safra's construction<br />for sequential Buchi automata. As in the sequential case, the blow-up<br />in the state space is essentially that of the underlying subset construction.
10
Bartholdi, Laurent, and Marialaura Noce. "Tree languages and branched groups." Mathematische Zeitschrift 303, no. 4 (March 20, 2023). http://dx.doi.org/10.1007/s00209-023-03249-y.
Full textAbstract:
AbstractWe study the portraits of isometries of rooted trees—the labelling of the tree, at each vertex, by the permutation of its descendants—in terms of languages. We characterize regularly branched self-similar groups in terms of $$\omega $$ ω -regular languages. We deduce the algorithmic decidability of some problems, such as the comparison of regularly branched contracting groups, and their orbit structure on the boundary of the rooted tree.
11
Jagtap, Pushpak, and Dimos V. Dimarogonas. "Controller synthesis against omega‐regular specifications: A funnel‐based control approach." International Journal of Robust and Nonlinear Control, March 25, 2024. http://dx.doi.org/10.1002/rnc.7339.
Full textAbstract:
AbstractThe paper focuses on the problem of formal synthesis of controllers for control‐affine nonlinear systems against complex properties. Our goal is to design a closed‐form control policy that guarantees the satisfaction of complex properties that are expressed using ()‐regular languages and equivalently recognized by nondeterministic Büchi automata (NBA). We propose leveraging a funnel‐based control approach to provide a closed‐form solution to the problem. Our approach decomposes the specification represented by NBA into a sequence of reachability problems, which we solve using a funnel‐based control approach. Controllers associated with each reachability problem are then combined to design a hybrid control policy enforcing the desired ()‐regular property. We demonstrate the effectiveness of the proposed results on room temperature control and mobile robot motion control case studies.
12
Winkler, Tobias, Christina Gehnen, and Joost-Pieter Katoen. "Model Checking Temporal Properties of Recursive Probabilistic Programs." Logical Methods in Computer Science Volume 19, Issue 4 (December 15, 2023). http://dx.doi.org/10.46298/lmcs-19(4:24)2023.
Full textAbstract:
Probabilistic pushdown automata (pPDA) are a standard operational model for programming languages involving discrete random choices and recursive procedures. Temporal properties are useful for specifying the chronological order of events during program execution. Existing approaches for model checking pPDA against temporal properties have focused mostly on $\omega$-regular and LTL properties. In this paper, we give decidability and complexity results for the model checking problem of pPDA against $\omega$-visibly pushdown languages that can be described by specification logics such as CaRet. These logical formulae allow specifying properties that explicitly take the structured computations arising from procedural programs into account. For example, CaRet is able to match procedure calls with their corresponding future returns, and thus allows to express fundamental program properties such as total and partial correctness.
13
Cimatti, Alessandro, Luca Geatti, Nicola Gigante, Angelo Montanari, and Stefano Tonetta. "A first-order logic characterization of safety and co-safety languages." Logical Methods in Computer Science Volume 19, Issue 3 (August 10, 2023). http://dx.doi.org/10.46298/lmcs-19(3:13)2023.
Full textAbstract:
Linear Temporal Logic (LTL) is one of the most popular temporal logics, that comes into play in a variety of branches of computer science. Among the various reasons of its widespread use there are its strong foundational properties: LTL is equivalent to counter-free omega-automata, to star-free omega-regular expressions, and (by Kamp's theorem) to the First-Order Theory of Linear Orders (FO-TLO). Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not belong or belongs to the language, respectively, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis for LTL. SafetyLTL (resp., coSafetyLTL) is a fragment of LTL where only universal (resp., existential) temporal modalities are allowed, that recognises safety (resp., co-safety) languages only. The main contribution of this paper is the introduction of a fragment of FO-TLO, called SafetyFO, and of its dual coSafetyFO, which are expressively complete with respect to the LTL-definable safety and co-safety languages. We prove that they exactly characterize SafetyLTL and coSafetyLTL, respectively, a result that joins Kamp's theorem, and provides a clearer view of the characterization of (fragments of) LTL in terms of first-order languages. In addition, it gives a direct, compact, and self-contained proof that any safety language definable in LTL is definable in SafetyLTL as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of SafetyLTL, interpreted over finite and infinite words. Moreover, we prove that, when interpreted over finite words, SafetyLTL (resp. coSafetyLTL) devoid of the tomorrow (resp., weak tomorrow) operator captures the safety (resp., co-safety) fragment of LTL over finite words.
14
Dave, V., E. Filiot, S. Krishna, and N. Lhote. "Synthesis of Computable Regular Functions of Infinite Words." Logical Methods in Computer Science Volume 18, Issue 2 (June 29, 2022). http://dx.doi.org/10.46298/lmcs-18(2:23)2022.
Full textAbstract:
Regular functions from infinite words to infinite words can be equivalently specified by MSO-transducers, streaming $\omega$-string transducers as well as deterministic two-way transducers with look-ahead. In their one-way restriction, the latter transducers define the class of rational functions. Even though regular functions are robustly characterised by several finite-state devices, even the subclass of rational functions may contain functions which are not computable (by a Turing machine with infinite input). This paper proposes a decision procedure for the following synthesis problem: given a regular function $f$ (equivalently specified by one of the aforementioned transducer model), is $f$ computable and if it is, synthesize a Turing machine computing it. For regular functions, we show that computability is equivalent to continuity, and therefore the problem boils down to deciding continuity. We establish a generic characterisation of continuity for functions preserving regular languages under inverse image (such as regular functions). We exploit this characterisation to show the decidability of continuity (and hence computability) of rational and regular functions. For rational functions, we show that this can be done in $\mathsf{NLogSpace}$ (it was already known to be in $\mathsf{PTime}$ by Prieur). In a similar fashion, we also effectively characterise uniform continuity of regular functions, and relate it to the notion of uniform computability, which offers stronger efficiency guarantees.
15
Gnatenko, Anton Romanovich, and Vladimir Anatolyevoch Zakharov. "USING AN EXTENSIONS OF CTL* FOR SPECIFICATION AND VERIFICATION OF SEQUENTIAL REACTIVE SYSTEMS." System Informatics, no. 17 (2020). http://dx.doi.org/10.31144/si.2307-6410.2020.n17.p21-32.
Full textAbstract:
Sequential reactive systems such as controllers, device drivers, computer interpreters operate with two data streams and transform input streams of data (control signals, instructions) into output streams of control signals (instructions, data). Finite state transducers are widely used as an adequate formal model for information processing systems of this kind. Since runs of transducers develop over time, temporal logics, obviously, could be used as both simple and expressive formalism for specifying the behavior of sequential reactive systems. However, the conventional applied temporal logics (LTL, CTL) do not suit this purpose well, since their formulae are interpreted over omega-languages, whereas the behavior of transducers are represented by binary relations on infinite sequences, i.e. omega-transductions. To provide temporal logic with the ability to take into account this general feature of the behavior of reactive systems, we introduced new extensions of this logic. Two distinguished features characterize these extension: 1) temporal operators are parameterized by sets of streams (languages) admissible for input, and 2) sets (languages) of expected output streams are used as basic predicates. In the previous series of works we studied the expressive power and the model checking problem for Reg-LTL and Reg-CTL which are such extensions of LTL and CTL where the languages mentioned above are regular ones. We discovered that such an extension of temporal logics increases their expressive capability though retains the decidability of the model checking problem. Our next step in the systematic study of expressive and algorithmic properties of new extensions temporal logics is the analysis of the model checking problem for finite state transducers against Reg-CTL* formulae. In this paper we develop a model checking algorithm for Reg-CTL* and show that this problem is in ExpSpace.
16
Bansal, Suguman, Swarat Chaudhuri, and Moshe Y. Vardi. "Comparator automata in quantitative verification." Logical Methods in Computer Science Volume 18, Issue 3 (July 29, 2022). http://dx.doi.org/10.46298/lmcs-18(3:13)2022.
Full textAbstract:
The notion of comparison between system runs is fundamental in formal verification. This concept is implicitly present in the verification of qualitative systems, and is more pronounced in the verification of quantitative systems. In this work, we identify a novel mode of comparison in quantitative systems: the online comparison of the aggregate values of two sequences of quantitative weights. This notion is embodied by comparator automata (comparators, in short), a new class of automata that read two infinite sequences of weights synchronously and relate their aggregate values. We show that aggregate functions that can be represented with B\"uchi automaton result in comparators that are finite-state and accept by the B\"uchi condition as well. Such $\omega$-regular comparators further lead to generic algorithms for a number of well-studied problems, including the quantitative inclusion and winning strategies in quantitative graph games with incomplete information, as well as related non-decision problems, such as obtaining a finite representation of all counterexamples in the quantitative inclusion problem. We study comparators for two aggregate functions: discounted-sum and limit-average. We prove that the discounted-sum comparator is $\omega$-regular iff the discount-factor is an integer. Not every aggregate function, however, has an $\omega$-regular comparator. Specifically, we show that the language of sequence-pairs for which limit-average aggregates exist is neither $\omega$-regular nor $\omega$-context-free. Given this result, we introduce the notion of prefix-average as a relaxation of limit-average aggregation, and show that it admits $\omega$-context-free comparators i.e. comparator automata expressed by B\"uchi pushdown automata.