Arrow Research search

Author name cluster

J.-J.Ch. Meyer

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers
1 author row

Possible papers

8

AIJ Journal 1999 Journal Article

A logical approach to the dynamics of commitments

  • J.-J.Ch. Meyer
  • W. van der Hoek
  • B. van Linder

In this paper we present a formalisation of motivational attitudes, the attitudes that are the driving forces behind the actions of agents. We consider the statics of these attitudes both at the assertion level, i. e. , ranging over propositions, and at the practition 2 The term `practition' is due to Castañeda [6]. 2 level, i. e. , ranging over actions, as well as the dynamics of these attitudes, i. e. , how they change over time. Starting from an agent's wishes, which form the primitive, most fundamental motivational attitude, we define its goals as induced by those wishes that do not yet hold, i. e. , are unfulfilled, but are within the agent's practical possibility to bring about, i. e. , are implementable for the agent. Among these unfulfilled, implementable wishes the agent selects those that qualify as its goals. Based on its knowledge on its goals and practical possibilities, an agent may make certain commitments. In particular, an agent may commit itself to actions that it knows to be correct and feasible to bring about some of its known goals. As soon as it no longer knows its commitments to be useful, i. e. , leading to fulfillment of some goal, and practically possible, an agent is able to undo these commitments. Both the act of committing as well as that of undoing commitments is modelled as a special model-transforming action in our framework, which extends the usual state-transition paradigm of Propositional Dynamic Logic. In between making and undoing commitments, an agent is committed to all the actions that are known to be identical for all practical purposes to the ones in its agenda. By modifying the agent's agenda during the execution of actions in a straightforward way, it is ensured that commitments display an intuitively acceptable behaviour with regard to composite actions.

TCS Journal 1988 Journal Article

Applications of compactness in the Smyth powerdomain of streams

  • J.-J.Ch. Meyer
  • E.P. de Vink

We show in a uniform setting the crucial role of compactness in the theory of the Smyth powerdomain of streams. The topological notion of compactness is characterized in an order- theoretical manner, involving a notion of bounded sets. We obtain general results on the continuity of operators, and consider applications as diverse as interleaving, hiding and stream programming operators.

TCS Journal 1987 Journal Article

Infinite streams and finite observations in the semantics of uniform concurrency

  • J.W. de Bakker
  • J.-J.Ch. Meyer
  • E.-R. Olderog

Two ways of assigning meaning to a language with uniform concurrency are presented and compared. The language has uninterpreted elementary actions from which statements are composed using sequential composition, nondeterministic choice, parallel composition with communication, and recursion. The first semantics uses infinite streams in the sense which is a refinement of the linear time semantics of De Bakker. The second semantics uses the finite observations of Hoare, situated ‘in between’ the divergence and readiness semantics of Olderog and Hoare. It is shown that the two models are isomorphic and that this isomorphism induces an equivalence result between the two semantics. Furthermore, a definition of the hiding operation which is inspired by the infinite streams approach is presented. Finally, the continuity of this operation is proved in the framework of finite observations.

TCS Journal 1986 Journal Article

Merging regular processes by means of fixed-point theory

  • J.-J.Ch. Meyer

First, we investigate a trace-set semantics of processes with μ-recursion and arbitrary interleaving (merge). μ-Recursion is the analogue of recursion in standard programming by means of a recursive procedure. Iteration using while-statements can be viewed as a special case of this: so-called regular recursion. The semantics is used to support a formalism that determines the merge of two regular sequential (nondeterministic) processes. Next, we turn to processes with merge, μ-recursion, and a second kind of recursion, called α-recursion. This kind of recursion when applied in a regular form is the equivalent of the Kleene-star iteration known from formal language theory. It involves only arbitrary big, but finite numbers of iterations. A different, more complicated framework is needed to give meaning to this kind of processes. Hereafter we define the semantics of the fair merge of these processes. Finally, we use this to prove the correctness of a formalism similar to the one for arbitrary merge in order to calculate the fair merge of two regular sequential (nondeterministic) processes with μ-recursion.

TCS Journal 1984 Journal Article

Linear time and branching time semantics for recursion with merge

  • J.W. de Bakker
  • J.A. Bergstra
  • J.W. Klop
  • J.-J.Ch. Meyer

We consider two ways of assigning semantics to a class of statements built from a set of atomic actions (the ‘alphabet’), by means of sequential composition, nondeterministic choice, recursion and merge (arbitrary interleaving). The first is linear time semantics (LT), stated in terms of trace theory; the semantic domain is the collection of all closed sets of finite and infinite words. The second is branching time semantics (BT), as introduced by De Bakker and Zucker; here the semantic domain is the metric completion of the collection of finite processes. For LT we prove the continuity of the operations (merge, sequential composition) in a direct, combinatorial way. Next, a connection between LT and BT is established by means of the operation trace which assigns to a process its set of traces. We show that the trace set of a process is closed and that trace is continuous. This requires the compactness of the semantic domains, ensured by the finiteness of the alphabet. Using trace, we then can carry over BT into LT.

TCS Journal 1983 Journal Article

On finite computations in denotational semantics

  • J.W. de Bakker
  • J.-J.Ch. Meyer
  • J.I. Zucker

Finite and, especially, infinite computations in languages with iteration or recursion are studied in the framework of denotational semantics, and a theorem is proved which relates their syntactic and semantic characterizations. A general proof method is presented to establish this type of relations, and it is shown how—in an induction on the structure of the syntactic constructs of the language—the recursive case follows from the non-recursive one by applying a general definitional scheme. The method is applicable to a variety of other problems concerning recursive constructs such as, for example, fixed point characterizations of several notions of weakest precondition. Also, the connections with the theory of languages with infinite words are discussed, in particular with a substitution theorem due to Nivat (1978).

TCS Journal 1982 Journal Article

On the elimination of iteration quantifiers in a fragment of algorithmic logic

  • J.A. Bergstra
  • J.-J.Ch. Meyer

In this paper we study the elimination of the iteration quantifier ∪ in a special set of algorithmic formulae. Something similar has been done by G. Mirkowska and E. Orlowska by means of a system of procedures. We, however, show that elimination is already possible by using the programs in our sublanguage itself.

v2026.09.13