scholarly journals Extended Temporal Logic on Finite Words and Wreath Product of Monoids with Distinguished Generators

2002 ◽  
Vol 9 (47) ◽  
Author(s):  
Zoltán Ésik
Keyword(s):  
Temporal Logic ◽  
Wreath Product ◽  
Expressive Power ◽  
Regular Languages ◽  
Modal Operator

We associate a modal operator with each language belonging to a given class of regular languages and use the (reverse) wreath product of monoids with distinguished generators to characterize the expressive power of the resulting logic.

scholarly journals On the Satisfiability and Model Checking for one Parameterized Extension of Linear-time Temporal Logic

2021 ◽  
Vol 28 (4) ◽  
pp. 356-371
Author(s):  
Anton Romanovich Gnatenko ◽  
Vladimir Anatolyevich Zakharov
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Linear Time ◽  
Complete Solution ◽  
Reactive Systems ◽  
Expressive Power ◽  
Regular Languages ◽  
Specification Languages ◽  
Temporal Logics ◽  
Emptiness Problem

Sequential reactive systems are computer programs or hardware devices which process the flows of input data or control signals and output the streams of instructions or responses. When designing such systems one needs formal specification languages capable of expressing the relationships between the input and output flows. Previously, we introduced a family of such specification languages based on temporal logics $LTL$, $CTL$ and $CTL^*$ combined with regular languages. A characteristic feature of these new extensions of conventional temporal logics is that temporal operators and basic predicates are parameterized by regular languages. In our early papers, we estimated the expressive power of the new temporal logic $Reg$-$LTL$ and introduced a model checking algorithm for $Reg$-$LTL$, $Reg$-$CTL$, and $Reg$-$CTL^*$. The main issue which still remains unclear is the complexity of decision problems for these logics. In the paper, we give a complete solution to satisfiability checking and model checking problems for $Reg$-$LTL$ and prove that both problems are Pspace-complete. The computational hardness of the problems under consideration is easily proved by reducing to them the intersection emptyness problem for the families of regular languages. The main result of the paper is an algorithm for reducing the satisfiability of checking $Reg$-$LTL$ formulas to the emptiness problem for Buchi automata of relatively small size and a description of a technique that allows one to check the emptiness of the obtained automata within space polynomial of the size of input formulas.

FINITE STATE PROCESSES, Z-TEMPORAL LOGIC AND THE MONADIC THEORY OF THE INTEGERS

1992 ◽  
Vol 03 (03) ◽  
pp. 233-244 ◽  
Author(s):  
A. SAOUDI ◽  
D.E. MULLER ◽  
P.E. SCHUPP
Keyword(s):  
Temporal Logic ◽  
Linear Temporal Logic ◽  
Second Order ◽  
Regular Languages ◽  
Infinite Words ◽  
First Order ◽  
Monadic Theory ◽  
Finite State ◽  
Temporal Formula

We introduce four classes of Z-regular grammars for generating bi-infinite words (i.e. Z-words) and prove that they generate exactly Z-regular languages. We extend the second order monadic theory of one successor to the set of the integers (i.e. Z) and give some characterizations of this theory in terms of Z-regular grammars and Z-regular languages. We prove that this theory is decidable and equivalent to the weak theory. We also extend the linear temporal logic to Z-temporal logic and then prove that each Z-temporal formula is equivalent to a first order monadic formula. We prove that the correctness problem for finite state processes is decidable.

Mirror, mirror in my hand: a duality between specifications and models of process behaviour

1996 ◽  
Vol 6 (4) ◽  
pp. 353-373 ◽  
Author(s):  
J. L. Fiadeiro ◽  
J. F. Costa
Keyword(s):  
Temporal Logic ◽  
Structural Property ◽  
Reactive Systems ◽  
Expressive Power ◽  
Seminal Paper ◽  
Process Specification ◽  
Temporal Specifications ◽  
Mirror Mirror

SummarySince Pnueli’s seminal paper in 1977, Temporal Logic has been used as a formalism for specifying and verifying the correctness of reactive systems. In this paper, we show that, besides its expressive power, Temporal Logic enjoys a very strong structural property: it is categorical on processes. That is, we show how temporal specifications (as theories) can be embedded in categories of process behaviour, and out of this adjunction we build an institution that is categorical in the sense of Meseguer. This characterisation means that temporal logic is, in a sense, ‘sound and complete’ with respect to process specification and interconnection techniques.

scholarly journals Positive Neural Networks in Discrete Time Implement Monotone-Regular Behaviors

2015 ◽  
Vol 27 (12) ◽  
pp. 2623-2660 ◽  
Author(s):  
Tom J. Ameloot ◽  
Jan Van den Bussche
Keyword(s):  
Neural Network ◽  
Neural Networks ◽  
Discrete Time ◽  
Expressive Power ◽  
Regular Languages ◽  
Regular Behavior ◽  
Multiple Input

We study the expressive power of positive neural networks. The model uses positive connection weights and multiple input neurons. Different behaviors can be expressed by varying the connection weights. We show that in discrete time and in the absence of noise, the class of positive neural networks captures the so-called monotone-regular behaviors, which are based on regular languages. A finer picture emerges if one takes into account the delay by which a monotone-regular behavior is implemented. Each monotone-regular behavior can be implemented by a positive neural network with a delay of one time unit. Some monotone-regular behaviors can be implemented with zero delay. And, interestingly, some simple monotone-regular behaviors cannot be implemented with zero delay.

scholarly journals Temporalising Separation Logic for Planning with Search Control Knowledge

2017 ◽  
Author(s):  
Xu Lu ◽  
Cong Tian ◽  
Zhenhua Duan
Keyword(s):  
Temporal Logic ◽  
Expressive Power ◽  
Separation Logic ◽  
Temporal Constraints ◽  
Ai Planning ◽  
Temporal Logics ◽  
Spatial Constraints ◽  
Spatio Temporal ◽  
Control Knowledge ◽  
Search Control

Temporal logics are widely adopted in Artificial Intelligence (AI) planning for specifying Search Control Knowledge (SCK). However, traditional temporal logics are limited in expressive power since they are unable to express spatial constraints which are as important as temporal ones in many planning domains. To this end, we propose a two-dimensional (spatial and temporal) logic namely PPTL^SL by temporalising separation logic with Propositional Projection Temporal Logic (PPTL). The new logic is well-suited for specifying SCK containing both spatial and temporal constraints which are useful in AI planning. We show that PPTL^SL is decidable and present a decision procedure. With this basis, a planner namely S-TSolver for computing plans based on the spatio-temporal SCK expressed in PPTL^SL formulas is developed. Evaluation on some selected benchmark domains shows the effectiveness of S-TSolver.

WEAKLY ITERATED BLOCK PRODUCTS AND APPLICATIONS TO LOGIC AND COMPLEXITY

2010 ◽  
Vol 20 (02) ◽  
pp. 319-341 ◽  
Author(s):  
HOWARD STRAUBING ◽  
PASCAL TESSON ◽  
DENIS THÉRIEN
Keyword(s):  
Wreath Product ◽  
Communication Complexity ◽  
Regular Languages ◽  
First Order ◽  
Bounded Depth Circuits ◽  
Decomposition Theorems ◽  
Block Product

Unlike the wreath product, the block product is not associative at the level of varieties. All decomposition theorems involving block products, such as the bilateral version of Krohn–Rhodes' theorem, have always assumed a right-to-left bracketing of the operands. We consider here the left-to-right bracketing, which is generally weaker. More precisely, we are interested in characterizing for any pseudovarieties of monoids U, V the smallest pseudovariety W that contains U and such that W □ V = W. This allows us to obtain new decomposition results for a number of important varieties such as DA, DO and DA * G. We apply these results to characterize the regular languages definable with generalized first-order sentences using only two variables and to shed new light on recent results on regular languages recognized by bounded-depth circuits with a linear number of wires and regular languages with small communication complexity.

Regular Languages Definable by Lindström Quantifiers (Preliminary Version)

2002 ◽  
Vol 9 (20) ◽  
Author(s):  
Zoltán Ésik ◽  
Kim G. Larsen
Keyword(s):  
Semidirect Product ◽  
Expressive Power ◽  
Regular Languages ◽  
Finite Monoid ◽  
Preliminary Version

In our main result, we establish a formal connection between Lindström quantifiers with respect to regular languages and the double semidirect product of finite monoid-generator pairs. We use this correspondence to characterize the expressive power of Lindström quantifiers associated with a class of regular languages.<br /><br />Superseded by BRICS-RS-03-28.

Sign in / Sign up

Export Citation Format

Share Document