Titlebook: Automata, Languages and Programming; 18th International C Javier Leach Albert,Burkhard Monien,Mario Rodrígue Conference proceedings 1991 Sp

率直

A Kleene theorem for infinite trace languages, generalized Kleene‘s theorem showing that the recognizable trace languages are exactly the co-rational languages. Besides, infinite traces have been recently introduced as a natural extension of both finite traces and infinite words. In this paper we generalize Kleene‘s theorem to languages of infi

adj忧郁的

modish

Logic programming with recurrence domains, certain recursive types. We present an extension of Horn logic programs, called ω-Prolog, which allows a finite schematization of infinitely many clauses via predicates with ω-terms as arguments. We show that for every ω-Prolog program there is an equivalent Horn logic program. That is, incorporati

Receive

Extensional embedding of a strongly stable model of PCF, performing simultaneously an extensional and a “stable” semantics in such a way that only maps existing in both semantics subsist in our model. The construction is carried out in the framework of strongly stable functions that we have recently defined and which is a refinement of stable semantics s

mydriatic

Uniform ideals and strictness analysis,ection for lazy list strictness analysis is not in general expressible as an abstract interpretation property of the standard semantics. We give circumstances when it is so expressible. Doing so casts light on Burn‘s .. projection and his question of its relationship to ...Uniform ideals are a gener

纵火

Logical and computational aspects of programming with sets/bags/lists,e can lack a meaning in the sense that their outputs may be sensitive to the choice of input expression. We are, thus, naturally lead to a set-theoretic denotational semantics with partial functions. We set up a logic for reasoning about the definedness of terms and a deterministic and terminating e

set598

Safety for branching time semantics,rties using a .. Then, we consider the case of branching time semantics where a program is modeled by a set of infinite computation trees modulo bisimulation. We propose and study a safety preorder for this semantics based on simulation and dealing with silent actions. We focus on regular safety pro

Lipohypertrophy

Program composition and modular verification,contributions of this paper include:.Modular termination proof systems that have been suggested before are defined for models with an unfair scheduler. The proof approach presented in them fails to be complete in a model with a fair scheduler. The main idea suggested here which allows for the develo

有杂色

Model-checking for probabilistic real-time systems,la. This paper extends model-checking to stochastic real-time systems, whose behavior depends on probabilistic choice and quantitative time. The specification language is ., a branching-time temporal logic for expressing real-time properties. We interpret the formulas of the logic over generalized s

FER

Computing behavioural relations, logically, behavioral relations between processes. The algorithm‘s complexity is proportional to the product of the size of the process and the size of the formula, and thus improves on the best existing algorithm for such a fixed point logic. The method for computing preorders that the model checker induces