Search

• A set of theories is presented over multi-matching nested relations, including words, expressions and automata. • A new temporal logic of multi-matching nested calls and returns (MNCARET) is proposed. • An approach to model check MNCARET formulas for the MNTA model is presented. Multi-matching nested relation consists of a sequence of linearly ordered positions, call , internal , and return , augmented with one-to-one, one-to-n or n-to-one matching nested edges from call to return. For clarity, inner-call and inner-return are defined in n-to-one and one-to-n matching nested relations respectively. After word encoding by introducing tagged letters, Multi-matching Nested Words (MNWs) are obtained over a tagged alphabet. Then Multi-matching Nested Expression (MNE) and Multi-matching Nested Traceable Automaton (MNTA) are defined over MNWs. The closure properties of languages over MNWs are studied, including union, intersection, concatenation, Kleene-* and complementation. Moreover, nondeterministic MNTAs are as expressive as deterministic ones. Further, a transformation method from MNTAs to MNEs is proposed, where three kinds of labeled arcs are created for different transitions in order for the specific merging strategies. To specify the requirements of multi-matching nested calls and returns , we propose a temporal logic of Multi-matching Nested CAlls and RETurns (MNCARET). The abstract and matched-abstract versions of modalities are considered. For example, abstract-next operator allows a path to jump from a call to the first matched non- internal , which is the inner-call , inner-return or return , in a one-to-n or n-to-one matching relation while matched-abstract-next operator from a call directly to the matched return. We also present an approach to model check MNCARET formulas for the MNTA model, a subset of pushdown automata. This problem is reduced to the emptiness problem of Büchi MNTAs. [ABSTRACT FROM AUTHOR]

To specify properties of open systems with interval based temporal logics, Alternating Projection Temporal Logic (APTL) is proposed by introducing Concurrent Game Structures (CGS) to Propositional Projection Temporal Logic (PPTL). Further, examples are given to show how properties of open systems can be specified by APTL formulas. Moreover, to establish the automata based model theory for the new proposed logic, Generalized alternating Büchi automata over Concurrent Game structures (GBCGs) are defined, and a transformation from APTL formulas to GBCGs is presented. In addition, a decision procedure for checking the satisfiability of APTL formulas, and a model checking approach for APTL with Concurrent Game Structures (CGSs) being models are presented. [ABSTRACT FROM AUTHOR]

Abstract: Eilenberg, Elgot and Shepherdson showed in 1969, [S. Eilenberg, C.C. Elgot, J.C. Shepherdson, Sets recognized by -tape automata, Journal of Algebra 13 (1969) 447–464], that a relation on finite words over a finite, non-unary alphabet with letters is definable in first order logic with predicates for the relations equal length, prefix and last letter is (for each letter ) if and only if it can be recognized by a finite multitape synchronous automaton, i.e., one whose read heads move simultaneously. They left open the characterization in the case of infinite alphabets, and proposed some conjectures concerning them. We solve all problems and sharpen the main theorem of [S. Eilenberg, C.C. Elgot, J.C. Shepherdson, Sets recognized by -tape automata, Journal of Algebra 13 (1969) 447–464]. [Copyright &y& Elsevier]

Abstract: We introduce a complexity measure of modal properties of finite structures which generalises the automaticity of languages. It is based on graph-automata-like devices called labelling systems. We define a measure of the size of a structure that we call rank, and show that any modal property of structures can be approximated up to any fixed rank by a labelling system. The function that takes to the size of the smallest labelling system doing this is called the labelling index of the property. We demonstrate that this is a useful and fine-grained measure of complexity and show that it is especially well suited to characterise the expressive power of modal fixed-point logics. From this we derive several separation results of modal and non-modal fixed-point logics, some of which are already known whereas others are new. [Copyright &y& Elsevier]

Abstract: We show that some simple and useful stutter-invariant properties definable in the language of Lamport''s Simple Temporal Logic of Actions (STLA) are not definable in STLA and present a natural extension of STLA that allows one to express all stutter-invariant properties definable in the language of STLA. [Copyright &y& Elsevier]

Abstract: We define a weighted monadic second order logic for trees where the weights are taken from a commutative semiring. We prove that a restricted version of this logic characterizes the class of formal tree series which are accepted by weighted bottom-up finite state tree automata. The restriction on the logic can be dropped if additionally the semiring is locally finite. This generalizes corresponding classical results of Thatcher, Wright, and Doner for tree languages and it extends recent results of Droste and Gastin [Weighted automata and weighted logics, in: Automata, Languages and Programming—32nd International Colloquium, ICALP 2005, Lisbon, Portugal, 2005, Proceedings, Lecture Notes in Computer Science, Vol. 3580, Springer, Berlin, 2005, pp. 513–525, full version in Theoretical Computer Science, to appear.] from formal power series on words to formal tree series. [Copyright &y& Elsevier]

Abstract: Periodicity constraints are used in many logical formalisms, in fragments of Presburger LTL, in calendar logics, and in logics for access control, to quote a few examples. In the paper, we introduce the logic , an extension of Linear-Time Temporal Logic LTL with past-time operators whose atomic formulae are defined from a first-order constraint language dealing with periodicity. Although the underlying constraint language is a fragment of Presburger arithmetic shown to admit a PSPACE-complete satisfiability problem, we establish that model-checking and satisfiability problems remain in PSPACE as plain LTL (full Presburger LTL is known to be highly undecidable). This is particularly interesting for dealing with periodicity constraints since the language of has a language more concise than existing languages and the temporalization of our first-order language of periodicity constraints has the same worst case complexity as the underlying constraint language. Finally, we show examples of introduction the quantification in the logical language that provide to , EXPSPACE-complete problems. As another application, we establish that the equivalence problem for extended single-string automata, known to express the equality of time granularities, is PSPACE-complete by designing a reduction from QBF and by using our results for . [Copyright &y& Elsevier]

Abstract: We present a compositional approach to defining expressive logics for coalgebras of endofunctors on . This approach uses a notion of language constructor and an associated notion of semantics to capture one inductive step in the definition of a language for coalgebras and of its semantics. We show that suitable choices for the language constructors and for their associated semantics yield logics which are both adequate and expressive w.r.t. behavioural equivalence. Moreover, we show that type-building operations give rise to corresponding operations both on language constructors and on their associated semantics, thus allowing the derivation of expressive logics for increasingly complex coalgebraic types. Our framework subsumes several existing approaches to defining logics for coalgebras, and at the same time allows the derivation of new logics, with logics for probabilistic systems being the prime example. [Copyright &y& Elsevier]

This paper explores the application of rewriting logic to the executable formal modeling of real-time and hybrid systems. We give general techniques by which such systems can be specified as ordinary rewrite theories, and show that a wide range of real-time and hybrid system models, including object-oriented systems, timed automata, hybrid automata, timed and phase transition systems, and timed extensions of Petri nets, can indeed be expressed in rewriting logic quite naturally and directly. Since rewriting logic is executable and is supported by several language implementations, our approach complements property-oriented methods and tools less well suited for execution purposes, and can be used as the basis for symbolic simulation and formal analysis of real-time and hybrid systems. The relationships with the timed rewriting logic approach of Kosiuczenko and Wirsing are also studied. [Copyright &y& Elsevier]