Arrow Research search

Author name cluster

John-Jules 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.

42 papers
2 author rows

Possible papers

42

JAAMAS Journal 2026 Journal Article

A Verification Framework for Agent Communication

  • Rogier M. van Eijk
  • Frank S. De Boer
  • John-Jules Ch. Meyer

Abstract In this paper, we introduce a verification method for the correctness of multiagent systems as described in the framework of ACPL (Agent Communication Programming Language). The computational model of ACPL consists of an integration of the two different paradigms of CCP (Concurrent Constraint Programming) and CSP (Communicating Sequential Processes). The constraint programming techniques are used to represent and process information, whereas the communication mechanism of ACPL is described in terms of the synchronous handshaking mechanism of CSP. Consequently, we show how to define a verification method for ACPL in terms of an integration of the verification methods for CCP and CSP. We prove formally the soundness of the method and discuss its completeness.

Details DOI

JAAMAS Journal 2026 Journal Article

Agent Programming in 3APL

  • Koen V. Hindriks
  • Frank S. De Boer
  • John-Jules Ch. Meyer

Abstract An intriguing and relatively new metaphor in the programming community is that of an intelligent agent. The idea is to view programs as intelligent agents acting on our behalf. By using the metaphor of intelligent agents the programmer views programs as entities which have a mental state consisting of beliefs and goals. The computational behaviour of an agent is explained in terms of the decisions the agent makes on the basis of its mental state. It is assumed that this way of looking at programs may enhance the design and development of complex computational systems. To support this new style of programming, we propose the agent programming language 3APL. 3APL has a clear and formally defined semantics. The operational semantics of the language is defined by means of transition systems. 3APL is a combination of imperative and logic programming. From imperative programming the language inherits the full range of regular programming constructs, including recursive procedures, and a notion of state-based computation. States of agents, however, are belief or knowledge bases, which are different from the usual variable assignments of imperative programming. From logic programming, the language inherits the proof as computation model as a basic means of computation for querying the belief base of an agent. These features are well-understood and provide a solid basis for a structured agent programming language. Moreover, on top of that 3APL agents use so-called practical reasoning rules which extend the familiar recursive rules of imperative programming in several ways. Practical reasoning rules can be used to monitor and revise the goals of an agent, and provide an agent with reflective capabilities. Applying the metaphor of intelligent agents means taking a design stance. From this perspective, a program is taken as an entity with a mental state, which acts pro-actively and reactively, and has reflective capabilities. We illustrate how the metaphor of intelligent agents is supported by the programming language. We also discuss the design of control structures for rule-based agent languages. A control structure provides a solution to the problem of which goals and which rules an agent should select. We provide a concrete and intuitive ordering on the practical reasoning rules on which such a selection mechanism can be based. The ordering is based on the metaphor of intelligent agents. Furthermore, we provide a language with a formal semantics for programming control structures. The main idea is not to integrate this language into the agent language itself, but to provide the facilities for programming control structures at a meta level. The operational semantics is accordingly specified at the meta level, by means of a meta transition system.

Details DOI

FLAP Journal 2023 Journal Article

Probabilistic Deontic Logics for Reasoning about Uncertain Norms.

  • Vincent de Wit
  • Dragan Doder
  • John-Jules Ch. Meyer

In this article, we present a proof-theoretical and model-theoretical approach to probabilistic logic for reasoning about uncertainty about normative state- ments. We introduce two logics with languages that extend both the language of monadic deontic logic and the language of probabilistic logic. The first logic allows statements like “the probability that one is obliged to be quiet is at least 0. 9”. The second logic allows iteration of probabilities in the language. We axiomatize both logics, provide the corresponding semantics and prove that the axiomatizations are sound and complete. We also prove that both logics are decidable. In addition, we show that the problem of deciding satisfiability for the simpler of our two logics is in PSPACE, no worse than that of deontic logic.

PDF Details

ECAI Conference 2016 Conference Paper

A Dynamic Logic of Norm Change

  • Max Knobbout
  • Mehdi Dastani
  • John-Jules Ch. Meyer

Norms are effective and flexible means to control and regulate the behaviour of autonomous systems. Adding norms to a system changes its specification which may in turn ensure desirable system properties. As of yet, there is no generally agreed formal methodology to represent and reason about the dynamics of norms and their impacts on system specifications. In this paper, we introduce various types of norms, such as state-based or action-based norms, and gradually develop a dynamic modal logic to characterize the dynamics of such norms in a formal way. The logic can be used to prove various properties of norm dynamics and their impacts on system specification. Moreover, we show that this logic is sound and complete.

Details

FLAP Journal 2015 Journal Article

Retalis Language for Information Engineering in Autonomous Robot Software.

  • Pouyan Ziafati
  • Mehdi Dastani
  • John-Jules Ch. Meyer
  • Leon van der Torre
  • Holger Voos

Robotic information engineering is the processing and management of data to create knowledge of the robot’s environment. It is an essential robotic tech- nique to apply AI methods such as situation awareness, task-level planning and knowledge-intensive task execution. Consequently, information engineering has been identified as a major challenge to make robotic systems more responsive to real-world situations. The Retalis language integrates ELE and SLR, two logic-based languages. Retalis is used to develop information engineering com- ponents of autonomous robots. In such a component, ELE is used for temporal and logical reasoning, and data transformation in flows of data. SLR is used to implement a knowledge base maintaining a history of events. SLR supports state-based representation of knowledge built upon discrete sensory data, man- agement of sensory data in active memories and synchronization of queries over asynchronous sensory data. In this paper, we introduce eight requirements for robotic information engineering, and we show how Retalis unifies and advances the state-of-the-art research on robotic information engineering. Moreover, we evaluate the efficiency of Retalis by implementing an application for a NAO robot. Retalis receives events about the positions of objects with respect to the top camera of NAO robot, the transformation among the coordinate frames of NAO robot, and the location of the NAO robot in the environment. About one thousand and nine hundreds events per second are processed in real-time to calculate the positions of objects in the environment.

PDF Details

ECAI Conference 2014 Conference Paper

An Agent-Based Model of Procrastination

  • Ruurdje Procee
  • Bart A. Kamphorst
  • Arlette van Wissen
  • John-Jules Ch. Meyer

Procrastination is a widespread type of self-regulation failure that can have serious negative effects on people's health (e. g. , because people delay or omit important health behaviors) and well-being. New "e-coaching" technologies make it possible in principle to offer tailored support to individuals in their efforts to change their self-undermining behavior. In practice, however, such automated support is currently unfeasible because the causal mechanisms behind procrastination are complex and poorly understood. This paper presents a new agent-based model of procrastination that integrates insights from economic models about the dynamics of procrastination with psychological concepts that can help explain the behavior on an individual level. The model is validated by using 5-fold cross validation with simulated annealing to fit and test the parameters on an existing dataset on academic procrastination (n=293). Results show that the agent displays realistic behavior and that the model with the fitted parameters performs significantly better (p<0. 01) than the model with randomly selected parameters.

Details

JELIA Conference 2014 Conference Paper

Reasoning about Dynamic Normative Systems

  • Max Knobbout
  • Mehdi Dastani
  • John-Jules Ch. Meyer

Abstract The use of normative systems is widely accepted as an effective approach to control and regulate the behaviour of agents in multi-agent systems. When norms are added to a normative system, the behaviour of such a system changes. As of yet, there is no clear formal methodology to model the dynamics of a normative system under addition of various types of norms. In this paper we view the addition of a norm as an update of a normative system, and we provide update semantics to model this process.

Details

EUMAS Conference 2011 Conference Paper

A Methodology for the Generation of Multi-agent Argumentation Dialogue Scenarios

  • Eric M. Kok
  • John-Jules Ch. Meyer
  • Herre van Oostendorp
  • Henry Prakken
  • Gerard Vreeswijk

Abstract Increasingly research into the uses of argumentation in multi-agent dialogues takes an experimental approach. Such studies explore how agents can successfully employ argumentation besides the best and worst case situations of formal analysis. While a vital part in these experiments is influenced by the scenarios from which dialogues are generated, there is very little research on how these can be generated in a meaningful way, respecting the characteristics of the underlying dialogue problem. This paper proposes, by means of an example system for deliberation dialogues, a methodology for the construction and evaluation of a scenario generation process. It is shown how scenarios can accommodate argumentation with structured arguments and how it is tested whether the generated scenarios are interesting for experimentation.

Details

AAMAS Conference 2011 Conference Paper

Multi-Criteria Argument Selection In Persuasion Dialogues

  • Tom L. van der Weide
  • Frank Dignum
  • John-Jules Ch. Meyer
  • H. Prakken
  • Gerard A. W. Vreeswijk

The main goal of a persuasion dialogue is to persuade, but agents may have a number of additional goals concerning the dialogue duration, how much and what information is shared or how aggressive the agent is. Several criteria have been proposed in the literature covering different aspects of what may matter to an agent, but it is not clear how to combine these criteria that are often incommensurable and partial. This paper is inspired by multi-attribute decision theory and considers argument selection as decision-making where multiple criteria matter. A meta-level argumentation system is proposed to argue about what argument an agent should select in a given persuasion dialogue. The criteria and sub-criteria that matter to an agent are structured hierarchically into a value tree and meta-level argument schemes are formalized that use a value tree to justify what argument the agent should select. In this way, incommensurable and partial criteria can be combined.

PDF

AAMAS Conference 2011 Conference Paper

Programming Mental State Abduction

  • Michal Sindlar
  • Mehdi Dastani
  • John-Jules Ch. Meyer

Many multi-agent system applications involve software agents that reason about the behavior of other agents with which they interact in cooperation or competition. In order to design and develop those systems, the employed programming languages should provide tools to facilitate the implementation of agents that can perform such reasoning. This paper focuses on BDI-based programming languages and proposes a nonmonotonic reasoning mechanism that can be incorporated into agents, allowing them to reason about observed behavior to infer others' beliefs or goals. In particular, it is suggested that the behavior-generating rules of agents are translated into a nonmonotonic logic programming framework. A formal analysis of the presented approach is provided and it is shown that it has desirable properties.

PDF

TCS Journal 2011 Journal Article

Reasoning about plan revision in BDI agent programs

  • Natasha Alechina
  • Mehdi Dastani
  • Brian Logan
  • John-Jules Ch. Meyer

Facilities for handling plan execution failures are essential for agents which must cope with the effects of nondeterministic actions, and some form of failure handling can be found in most mature agent programming languages and platforms. While such features simplify the development of more robust agents, they make it hard to reason about the execution of agent programs, e. g. , to verify their correctness. In this paper, we present an approach to the verification of agent programs which admit exceptional executions. We consider executions of the BDI-based agent programming language 3APL in which plans containing non-executable actions can be revised using plan revision rules, and present a logic for reasoning about normal and exceptional executions of 3APL programs. We provide a complete axiomatization for the logic and, using a simple example, show how to express properties of 3APL programs as formulas of the logic.

Details DOI

ECAI Conference 2010 Conference Paper

Mental State Ascription Using Dynamic Logic

  • Michal P. Sindlar
  • Mehdi Dastani
  • John-Jules Ch. Meyer

In situations where the behavior of a system must be interpreted because its state is not accessible, it is useful to explain observed behavior in mentalistic terms. This paper presents a formalism based on propositional dynamic logic to model ascription of beliefs, goals, or plans on grounds of observed actions. The formalism is used to provide semantics for an existing approach to abducing the mental state of an observed agent; in doing so it is shown how behavior-producing rules can be given different explanatory interpretations.

Details

LORI Conference 2009 Conference Paper

An Update Operator for Strategic Ability

  • Paolo Turrini
  • Jan M. Broersen
  • Rosja Mastop
  • John-Jules Ch. Meyer

Abstract Coalition Logic does not explicitly talk about the effects of a coalitional move on the strategic ability of the remaining players, while in Game Theory reasoning patterns involving this concept often occur. To fill this gap, we study an update operator for strategic ability update in coalition structures. Its formal connections with the update operators known from Dynamic Epistemic Logic will be discussed.

Details

JAAMAS Journal 2009 Journal Article

Coping with shame and sense of guilt: a Dynamic Logic Account

  • Paolo Turrini
  • John-Jules Ch. Meyer
  • Cristiano Castelfranchi

Abstract Aim of this work is to provide a formal characterization of those emotions that deal with normative reasoning, such as shame and sense of guilt, to understand their relation with rational action and to ground their formalization on a cognitive science perspective. In order to do this we need to identify the factors that constitute the preconditions and trigger the reactions of shame and sense of guilt in cognitive agents, that is when agents feel ashamed or guilty and what agents do when they feel so. We will also investigate how agents can induce and silence these feelings in themselves, i. e. the analysis of defensive strategies they can employ. We will argue that agents do have control over their emotions and we will analyze some operations they can carry out on them.

Details DOI

LORI Conference 2009 Conference Paper

Intentions and Assignments

  • Emiliano Lorini
  • Mehdi Dastani
  • Hans van Ditmarsch
  • Andreas Herzig
  • John-Jules Ch. Meyer

Abstract The aim of this work is propose a logical approach to intention dynamics based on the notion of assignment [3, 7]. The function of an assignment is to associate the truth value of a certain formula ϕ to a propositional atom p. We combine a static modal logic of belief and choice with three kinds of dynamic modalities and corresponding three kinds of assignments: assignments operating on an agent’s beliefs, assignments operating on the agent’s choices and assignments operating on the objective world. An agent’s intention is defined in our approach as the agent’s choice to perform a given action and two basic operations on intentions called intention generation and intention reconsideration are defined as specific kinds of assignments on choices.

Details

ECAI Conference 2008 Conference Paper

A Formal Model of Emotions: Integrating Qualitative and Quantitative Aspects

  • Bas R. Steunebrink
  • Mehdi Dastani
  • John-Jules Ch. Meyer

When constructing a formal model of emotions for intelligent agents, two types of aspects have to be taken into account. First, qualitative aspects pertain to the conditions that elicit emotions. Second, quantitative aspects pertain to the actual experience and intensity of elicited emotions. In this paper, we show how the qualitative aspects of a well-known psychological model of human emotions can be formalized in an agent specification language and how its quantitative aspects can be integrated into this model. Furthermore, we discuss several unspecified details and implicit assumptions in the psychological model that are explicated by this effort.

Details

JELIA Conference 2008 Conference Paper

A Logic for Closed-World Interaction

  • Jan M. Broersen
  • Rosja Mastop
  • John-Jules Ch. Meyer
  • Paolo Turrini

Abstract The aim of the work is to provide a language to reason about closed-world interaction, that is all those situations in which the outcomes of an interaction can be determined by the agents themselves and in which Nature does not play an active role. We formalize this intuition by identifying all such interactions and axiomatizing their logic. We apply the formal tools to reason about games and their regulation.

Details

JAAMAS Journal 2008 Journal Article

Goals in conflict: semantic foundations of goals in agent programming

  • M. Birna van Riemsdijk
  • Mehdi Dastani
  • John-Jules Ch. Meyer

Abstract This paper addresses the notion of (declarative) goals as used in agent programming. Goals describe desirable states, and semantics of these goals in an agent programming context can be defined in various ways. We focus in this paper on the representation of conflicting goals. In particular, we define two semantics for goals, one for unconditional goals and one for conditional goals. The first is based on propositional logic, and the latter is based on default logic. We establish relations between and properties of these semantics.

Details DOI

ECAI Conference 2008 Conference Paper

Magic Agents: Using Information Relevance to Control Autonomy

  • Bob van der Vecht
  • Frank Dignum
  • John-Jules Ch. Meyer

Autonomous agents are believed to have control over their internal state and over their behaviour. For that reason, an agent should control how and by whom it is being influenced. We introduce a reasoning component for BDI-agents that deals with the control over external influences, and we propose heuristics using local knowledge to process incoming stimuli. One of those heuristics is based on information relevance with respect to the agent's current plans and goals. We have developed a way to determine the relevance of information in BDI-agents using magic sets from database research as basis. The method presented shows a new application of magic sets by applying the theory in agent systems.

Details

AAMAS Conference 2008 Conference Paper

Multi-Agent Plan Diagnosis and Negotiated Repair

  • Huib Aldewereld
  • Pieter Buzing
  • Geert Jonker
  • Femke de Jonge
  • Frank Dignum
  • John-Jules Ch. Meyer
  • Nico Roos
  • Cees Witteveen

In the complex, dynamic domain of Air Traffic Control (ATC) many unexpected events can happen during the execution of a plan. Sometimes these disruptions make the plan infeasible and require a change of the original plan. Unexpected events may disrupt the execution of a plan leading to conflicts concerning the use of shared resources. By monitoring the possibly disrupted execution of a plan, air traffic controllers identify and repair conflicts before they occur, making the plan ‘healthy’ again. Model-based diagnosis helps to identify the causes of observed disruptions in the execution of a plan. This information enables the creation of better plan repairs. These repairs should efficient, but moreover they should be fair, i. e. , one airline should not be the victim of conflicts caused by another. Due to the complexity of planning tasks, it is beneficial to provide a distributed solution such that the workload is spread instead of centralised. Moreover, since the choice between various possible solutions to a conflict in the plan execution directly influence different parties (with diverting interests), the decision about which solution to choose should not be made by a single (central) decision maker, but agreed upon by the different parties involved. The Multi-Agent Diagnosis and negotiated repair (MAD) demonstrator combines our previous research done on model-based diagnosis, planning and scheduling techniques, and methods for multi-agent negotiation to solve this problem in a distributed manner. The resulting tool is a system to support the control and adaptation of distributed plan execution in the domain of ATC.

PDF

ECAI Conference 2008 Conference Paper

Organizing Coherent Coalitions

  • Jan M. Broersen
  • Rosja Mastop
  • John-Jules Ch. Meyer
  • Paolo Turrini

In this paper we provide and discuss a language to talk about coherence, a property of interaction that ensures players' abilities non to contradict one other and the empty coalition not to make active choices. With this property we can model a closed-world interaction, such as those of a Coordination Game or of a Prisoner Dilemma, where all the outcomes are determined only by the choices of the agents that are present.

Details

KR Conference 2008 Conference Paper

Reasoning about Agent Deliberation

  • Natasha Alechina
  • Mehdi Dastani
  • Brian S. Logan
  • John-Jules Ch. Meyer

We present a family of sound and complete logics for reasoning about deliberation strategies for SimpleAPL programs. SimpleAPL is a fragment of the agent programming language 3APL designed for the implementation of cognitive agents with beliefs, goals and plans. The logics are variants of PDL, and allow us to prove safety and liveness properties of SimpleAPL agent programs under different deliberation strategies. We show how to axiomatize different deliberation strategies for SimpleAPL programs, and, for each strategy we consider, prove a correspondence between the operational semantics of SimpleAPL and the models of the corresponding logic. We illustrate the utility of our approach with an example in which we show how to verify correctness properties for a simple agent program under different deliberation strategies.

AAMAS Conference 2007 Conference Paper

A Formal Road from Institutional Norms to Organizational Structures

  • Davide Grossi
  • Frank Dignum
  • John-Jules Ch. Meyer

Up to now, the way institutions and organizations have been used in the development of open systems has not often gone further than a useful heuristics. In order to develop systems actually implementing institutions and organizations, formal methods should take the place of heuristic ones. The paper presents a formal semantics for the notion of institution and its components (abstract and concrete norms, empowerment of agents, roles) and defines a formal relation between institutions and organizational structures. As a result, it is shown how institutional norms can be refined to constructs–organizational structures–which are closer to an implemented system. It is also shown how such a refinement process can be fully formalized and it is therefore amenable to rigorous verification.

PDF

AAMAS Conference 2007 Conference Paper

A Grounded Specification Language for Agent Programs

  • Mehdi Dastani
  • M. Birna van Riemsdijk
  • John-Jules Ch. Meyer

This paper studies the relation between agent specification and agent programming languages. In particular, it shows that an agent programming language obeys some desirable properties expressed in an agent specification language, i. e. , that any agent implemented by the programming language satisfies the desirable property expressed in the specification language. We study this relation by defining and aligning the semantics of an agent specification language and implementation language, and prove that certain properties expressed in the specification language are satisfied by the implementation language.

PDF

AAMAS Conference 2007 Conference Paper

Practical Extensions in Agent Programming Languages

  • Mehdi Dastani
  • Dirk Hobo
  • John-Jules Ch. Meyer

This paper proposes programming constructs to improve the practical application of existing BDI-based agent-oriented programming languages that have formal semantics. The proposed programming constructs include operations such as testing, adopting and dropping declarative goals, different execution modes for plans, repairing plans when their execution fail, event and exception handling mechanisms, and interfaces to existing imperative and declarative programming languages.

PDF

ECAI Conference 2006 Conference Paper

Goal Types in Agent Programming

  • Mehdi Dastani
  • M. Birna van Riemsdijk
  • John-Jules Ch. Meyer

This paper presents three types of declarative goals: perform goals, achieve goals, and maintain goals. The integration of these goal types in a simple but extendable logic-based agent-oriented programming language is discussed and motivated. The computational semantics for each goal type is presented by means of a transition system. It is shown that the presented semantics of the goal types ensure some desirable and expected properties.

Details

ECAI Conference 2006 Conference Paper

Programming Agents with Emotions

  • Mehdi Dastani
  • John-Jules Ch. Meyer

This paper presents the syntax and semantics of a simplified version of a logic-based agent-oriented programming language to implement agents with emotions. Four types of emotions are distinguished: happiness, sadness, anger and fear. These emotions are defined relative to agent's goals and plans. The emotions result from the agent's deliberation process and influence the deliberation process. The semantics of each emotion type is incorporated in the transition semantics of the presented agent-oriented programming language.

Details

TCS Journal 2006 Journal Article

Semantics of plan revision in intelligent agents

  • M. Birna van Riemsdijk
  • John-Jules Ch. Meyer
  • Frank S. De Boer

In this paper, we give an operational and denotational semantics for a meta-language of the 3APL agent programming language. With this meta-language, various 3APL interpreters can be programmed. We prove equivalence of the operational and denotational semantics. Furthermore, we give an operational semantics for object-level 3APL. Using this semantics, we relate the 3APL meta-language to object-level 3APL by providing a specific interpreter, the semantics of which will prove to be equivalent to object-level 3APL.

Details DOI

TCS Journal 2003 Journal Article

A fully abstract model for the exchange of information in multi-agent systems

  • Frank S. De Boer
  • Rogier M. van Eijk
  • Wiebe van der Hoek
  • John-Jules Ch. Meyer

In this paper, 1 1 This paper is an extended version of [7]. we present a semantic theory for the exchange of information in multi-agent systems. We consider the multi-agent programming language agent communication programming language, which integrates the paradigms of concurrent constraint programming and communicating sequential processes (CSP). The constraint programming techniques are used to represent and process information, whereas the synchronous communication mechanism from CSP is generalised to enable the exchange of information. The semantics of the language, which is based on a generalisation of traditional failure semantics, is shown to be fully abstract with respect to observing of each terminating computation its final global store of information.

Details DOI

NMR Workshop 2002 Conference Paper

The mutual exclusion problem in reasoning about action and change

  • Jan M. Broersen
  • John-Jules Ch. Meyer
  • Roel J. Wieringa

We describe a new aspect of the qualification problem that arises in the context of concurrent action. The qualification problem is typically approached by formulating principles of maximal qualification. However, for concurrent action the qualification problem is exponentionally harder, because we have to specify all mutual exclusions explicitly. We identify the problem encountered as ‘the mutual exclusion problem’. We argue that its solution may involve a default position regarding the qualification of concurrent actions relative to the qualification of constituent concurrent parts of an action. We describe the mutual exclusion problem in detail and propose a possible solution in terms of intended modal action models.

Details

TIME Conference 2001 Conference Paper

Reasoning about agents in the KARO framework

  • Ullrich Hustadt
  • Clare Dixon
  • Renate A. Schmidt
  • Michael Fisher 0001
  • John-Jules Ch. Meyer
  • Wiebe van der Hoek

This paper proposes two methods for realising automated reasoning about agent-based systems. The framework for modelling intelligent agent behaviour that we focus on is a core of KARO logic, an expressive combination of various modal logics including propositional dynamic logic, a modal logic of knowledge, a modal logic of wishes, and additional non-standard operators. The first method we present is based on a translation of core KARO logic to first-order logic combined with first-order resolution. The second method uses an embedding of core KARO logic into a combination of branching-time temporal logic CTL and multi-modal S5 plus a clausal resolution calculus for these combined logics. We discuss the advantages and shortcomings of each approach and suggest ways to extend each variant to cover more of the KARO framework.

Details

JELIA Conference 2000 Conference Paper

A Modal Logic for Network Topologies

  • Rogier M. van Eijk
  • Frank S. de Boer
  • Wiebe van der Hoek
  • John-Jules Ch. Meyer

Abstract In this paper, we present a logical framework that combines modality with a first-order quantification mechanism. The logic differs from standard first-order modal logics in that quantification is not performed inside the states of a model, but the states in the model themselves constitute the domain of quantifi-cation. The locality principle of modal logic is preserved via the requirement that in each state, the domain of quantification is restricted to a subset of the entire set of states in the model. We show that the language is semantically characterised by a generalisation of classical bisimulation, called history-based bisimulation, consider its decidability and study the application of the logic to describe and reason about the topologies of multi-agent systems.

Details

TARK Conference 1994 Conference Paper

An Epistemic Proof System for Parallel Processes

  • M. van Hulst
  • John-Jules Ch. Meyer

A proof system for the correctness of parallel programs using knowledge in distributed systems is presented and proven sound and relatively complete with respect to a formal Kripke style semantics that supports truly concurrent computations.

Details

MFCS Conference 1989 Conference Paper

Pomset Semantics for True Concurrency with Synchronization and Recursion (Extended Abstract)

  • John-Jules Ch. Meyer
  • Erik P. de Vink

Abstract In this paper we present a denotational semantics based on pomsets for a simple language with true concurrency, synchronization and recursion. In particular, we show how we can generalize standard techniques for stream-based linear-time interleaving models to yield continuous functions associated with the syntactic operators on the domain of sets of pomsets.

Details
v2026.09.13