This paper combines the classical model of labeled transition systems with the epistemic model for reasoning about knowledge. The result is a unifying framework for modeling and analyzing multi-agent, knowledge-based, dynamic systems. On the modeling side, we propose a process algebraic, agentoriented specification language that makes such a framework easy to use for practical purposes. On the verification side, we define a modal logic encompassing temporal and epistemic operators.
The formal modeling of agent-based systems and the knowledge transfer enabled by the related interactions is a research field common to several areas, ranging from concurrency theory to epistemic logic.
In the former setting, two basic models are mainly adopted to describe the dynamics of
systems: () Kripke structures are graphs where the nodes are annotated with atomic propositions
stating what is true in the system state associated with the node, and () labeled transition
systems (LTSs) are graphs where the arcs are annotated with actions representing the events
causing a change of system state. Both paradigms are equipped with temporal logics for the
description of properties, like, e.g., Computation Tree Logic (CTL) for state-based structures [
In the latter setting, the focus is on reasoning about knowledge from the viewpoint of
nonomniscient agents in terms of their capability of distinguishing diferent scenarios [
The connections between the two strands of research are evident and, in some cases, the
mutual foundational influence between traditional concurrency models and epistemic models
is investigated (see, e.g., [
The main goal of the paper is to combine the advantages of the two approaches by merging in a novel framework the capability of the LTS-based semantics of modeling dynamic, temporal behaviors with the capability of the epistemic models of representing what agents know or do not know. The rough idea behind the combination is associating a Kripke model with each state of an LTS. As additional contributions, this novel framework is enriched with a logic including dynamic and epistemic modalities and a high-level, process-algebraic specification language.
In the following, we introduce the model of Kripke labeled transition systems (Section 2) as a combination of epistemic models and LTSs. We define a logic for describing properties for such a model and establish the equivalence relation that is characterized by the logic. Then, we propose a process algebraic language for modeling agent-oriented concurrent systems with semantics based on Kripke labeled transition systems (Section 3). To emphasize the usability of this language, we describe a case study based on a popular, classical board game (Section 4). Finally, we discuss related work and potential future directions (Section 5).
Let be a set of agents (ranging over , , . . .), a set of actions (ranging over , ′, . . .), and a set of atomic propositions (ranging over , , . . .); we will use , , . . . to denote subsets of . First of all, we recall the definitions of labeled transition system and multi-agent epistemic model.
Definition 1. A labeled transition system (LTS) is a tuple (, , 0) where is a non-empty set of states (with 0 the initial state) and ⊆ × × is the action-labeled transition relation.
In the setting of computation modeling, LTSs describe the evolving behavior of discrete systems, where the actions labeling the transitions represent events leading from one configuration of the system to another.
Definition 2. A multi-agent epistemic model (called Kripke model) is a tuple (, { | ∈ }, ), where is a non-empty set of states; for every ∈ , ∈ 2× is a binary (accessibility) relation over ; : → 2 is a valuation function assigning to each state the set of propositions that hold in the state.
A pointed (resp., rooted) Kripke model is a pair ((, { | ∈ }, ), ), where ∈ is the current (resp., initial) state. Kripke models serve as the basis of the semantics for various modal logics and, in the case of epistemic languages, allow us to reason about knowledge in terms of information accessibility.
For our purposes, combining the dynamic action-based nature of LTSs with the possible worlds description of Kripke models results in action-based systems, the states of which are associated with accessibility relations and valuations. : → 2 is a valuation function.
A Kripke labeled transition system (KLTS) is a tuple (, , { | ∈ }, ), where : → 2 is a non-empty set of states; ⊆ ×
× is a transition relation; for every ∈ , 2
× 2 is a function mapping each state to a binary (accessibility) relation over 2; Pointed and rooted KLTSs are defined as expected. Firstly, states should not be considered dependent on atomic propositions. They are primitive semantic objects so that the set of propositions satisfied by a state does not uniquely identify the state. Secondly, each accessibility relation () relates elements of 2 and expresses the actual observational power of agent in state with respect to the truth of the propositions in . In other words, () describes the distinguishing power of agent in , intended as her capability of distinguishing the possible worlds identified by the values of the propositions. Under the indistinguishability interpretation of epistemic logic, () expresses informational indistinguishability between possible worlds. More precisely, (, ) ∈ () means that in the agent has insuficient information to establish whether we are in a state in which all and only the propositions of hold or in a state in which all and only the propositions of hold. Hence, both and are compatible with the knowledge of the agent in . By virtue of this interpretation, in the following we assume that the accessibility relations are equivalence relations. Thirdly, the transition relation and the valuation function are interpreted as usual.
Example 1. If ({} ∪ , {} ∪ ) belongs to () for any choice of , ∈ 2, then, in , all the possible worlds in which holds are mutually indistinguishable from the viewpoint of agent . If we also have that ({} ∪ , ) ̸∈ () whenever ̸∈ , we conclude that agent distinguishes all and only the pairs of worlds difering for the valuation of . Later, we will realize that this means that, in , agent knows the truth value of and is ignorant of any other proposition. Remark 1. From a rooted KLTS, an LTS can be derived. In particular, if we omit from a rooted KLTS ((, , _, _), 0) the accessibility relations and the valuation function, we obtain an LTS. Moreover, the KLTS (2, ∅, { | ∈ }, id ) – where each state represents a subset of , id is the identity function, and () = (′) for all ∈ and for any , ′ ∈ 2 – is a Kripke model.
LTSs and Kripke models provide the semantics for interpreting properties expressed in various modal logics. Inspired by temporal logics and epistemic logics, we propose a modal logic that naturally combines temporal and epistemic ingredients, called Kripke Temporal (KT) logic.
layers grammar:
The language ℒ of the KT logic is defined by the following two → → ⊤ | | ¬ | ∧ | ⟨ ⟩ | ⊤ | | ¬ |
∧ |
The formulas are called epistemic formulas. Note that the KT logic results from the
combination and encompasses both HML [
Definition 5. Given a KLTS := (, , { | ∈ }, ) and denoted := (2, {() |
∈ }, ), with ∈ , the truth of ∈ ℒ at ∈ , written , |= , is defined as follows:
1. , |= ⊤
2. , |= iff ∈ ()
3. , |= ¬ iff , ̸|=
4. , |= 1 ∧ 2 iff , |= 1 and , |= 2
5. , |= ⟨ ⟩ iff ∃′. (, , ′) ∈ and , ′ |=
6. , |= iff , () |=K , where the relation |=K is defined as:
() , |=K ⊤
() , |=K iff ∈
() , |=K ¬ iff , ̸|=K
() , |=K 1 ∧ 2 iff , |=K 1 and , |=K 2
() , |=K iff ∀. (, ) ∈ () : , |=K
Note that the formula is evaluated in ∈ with respect to the accessibility relations
associated with , thus emphasizing the view of the KLTS as an LTS where each state is
equipped with a Kripke model := (2, {() | ∈ }, ) 1. Hence, the semantics of
an epistemic formula evaluated in depends on such a Kripke model (|=K is the classical
satisfiability relation for Kripke models). By virtue of the indistinguishability interpretation we
adopted, since we are assuming to work with accessibility relations that are reflexive, symmetric,
and transitive, the reference system for the knowledge modality is S5 [
Based on the semantics above, two states and ′ are modal equivalent, written ≡ ′, if and only if they satisfy the same formulas. The KT logic characterizes the following notion of behavioral equivalence.
Definition 6. Let (, , { | ∈ }, ) be a KLTS. A binary equivalence relation on is a bisimulation if whenever (, ) ∈ then: 1. () = (); 2. if (, , ′) ∈ then ∃′. (, , ′) ∈ and (′, ′) ∈ ; 3. there exists a binary equivalence relation ℬ between the worlds of the Kripke models (2, {() | ∈ }, id ) pointed at () and (2, {() | ∈ }, ) pointed at (), such that ((), ()) ∈ ℬ and for any , ∈ 2, whenever (, ) ∈ ℬ then: • = ; • if (, ′) ∈ () for ∈ , then ∃ ′. (, ′) ∈ () and ( ′, ′) ∈ ℬ.
Note that conditions 1. and 3. resemble the definition of modal bisimulation for Kripke
models [
As a consequence of the grammar structure and the semantics of the KT logic, decidability and verification algorithms are inherited from the results related to epistemic logic and HML.
In this section, we define a process-algebraic, agent-oriented language with value passing, the
semantics of which is given in terms of KLTSs. We start by defining a basic calculus (see, e.g.,
[
The constant 0 stands for the inactive, halted process. The summation operator represents a nondeterministic choice enacting one of the guarded process terms ., which executes action and then behaves as process term (we will use to denote a non-empty summation). The constant is used to express recursive processes with ≥ 0 parameters, and must be associated with a defining equation of the form (1, . . . , ) := . The notation stands for any action, which can be an internal action (including the unobservable action ), an input action (, ), an output action ¯(, ), or an assignment action set (, ).
An assignment action has the efect of setting the proposition to the boolean value . An output action communicates an epistemic formula to the agent , while an input action receives a formula assigned to the variable from an agent assigned to the variable .
As usual in calculi with value passing, each occurrence of any variable in a process term is bound by either an input action or a constant definition. For instance, is bound in () := ¯(, ∧ ) . ( + 1) and in (, ) . ¯(, ⊤) . 0, but not in ¯(, ∧ ) . 0. Moreover, we write / and / for substitutions of values for variables, and denote by [/, / ] the result of substituting (resp., ) for all free (not bound) occurrences of (resp., ) in .
Formally, the behavior of a process term is described in structural operational semantics style as the LTS rooted at and defined by the transition relation ⊆ ℒ × Act × ℒ that is the least transition relation generated by the axioms and the rules in Table 1. All the preand post-conditions associated with knowledge-based behaviors (i.e., communications and assignments) will be defined when introducing the parallel composition of process terms and the knowledge structures. (1, . . . , ) := and each evaluates to (prefix) . →−−
(, ) set(, ) . →−− set(,) ¯(, ) . →−− ¯(, ) (input ) (, ) . →−−
[/, / ] for any ∈ and epistemic formula (recursion)
(sum) [1/1, . . . , / →]−− (1, . . . , →)−− . →−− . + →−− ′ ′ 3.1. Agents and pool of agents the actions as defined by the semantic rule: Process terms represent behavioral patterns of agents, while an agent is an instance of a process term with a unique identity. Several agents may communicate with each other to form a network of agents. Hence, we need to formalize the notion of agent and how agents interact in a so-called pool of agents. A dynamic knowledge structure will be added to regulate such interactions.
Agents are described by tuples of the form ⟨ ∈ , ∈ ℒ⟩ and are ranged over by ℐ, , . . .. The semantics of ⟨, ⟩ is given by the LTS expressing the behavior of , up to the renaming of (agent ) →−− . ⟨, ⟩→−− ⟨ ′ , ′⟩
So far, we abstracted from the interaction among agents and the underlying knowledge base. Now, we combine the behavior of several agents by integrating the notion of knowledge, which will allow us to specify how they can interact.
A pool of agents is a tuple (∪ℐ, ∪, ), where, for ranging over : • ∪ℐ denotes a finite set of agents; • ∪ denotes a finite set of binary accessibility relations over 2; • ⊆ is the set of true propositions. of the cartesian product ( × ℒ
The behavior of the set ∪ℐ depends on the behavior of each ℐ and is defined as an element ), where denotes the cardinality (i.e., the number of agents) of the pool. Then, for each agent , the accessibility relation expresses the capability of to − ′ = ∖{(, ′) | diff (, , ′, )} − ′ = closure( ∪ {({} ∪ , ) | ̸∈ } ∪ {(, {} ∪ ) | ̸∈ })
and, for := (2, ∪̸= ∪ , ) : (com) (∪̸=, ℐ ∪ ℐ ∪ , ∪̸= ∪ , ) |=
.a¯(j , ) ℐ →−− ℐ
.a(i, ) ′ →−− ′ ̸= (∪̸=, ℐ ∪ ℐ ∪ , ∪̸= ∪ , )→−−
(∪̸=, ℐ ∪ ℐ′ ∪ ′, ∪̸= ∪ ′ , ) where, for := (2, ∪̸= ∪ , ) : ′ = ∖{(, ′) | diff (, , ′, )} diff (, , , ) := (, |=K ∧ , ̸|=K ) ∨ (, ̸|=K ∧ , |=K )
closure() := ∪ {(, ) | ∃. (, ) ∈ ∧ (, ) ∈ } distinguish the possible worlds based on the values that can be attributed to the propositions of At . Finally, set denotes the current truth assignment for the propositions of At .
The agents of a pool can perform actions, either synchronously or autonomously, thus making the system dynamic. On the one hand, the internal actions that are not related to knowledge and the assignment actions represent the autonomous actions of agents. On the other hand, input and output actions represent synchronous communications that express knowledge transfer between agents.
Formally, such a joint knowledge-based and action-based behavior is represented by a KLTS describing the evolution of the pool of agents. is given by the KLTS ((, , ∪, ), ) rooted at , which is built as follows:
Let := (∪ℐ, ∪, ) be a pool of agents of cardinality . The semantics of () = . • the states in are pool tuples, where ∈ is the initial state; • is the least transition relation generated by the rules of Table 2; • for each ∈ of the form (_, ∪, ), it holds that () = for each ∈ and We now illustrate the rules of Table 2. The rule (pool ) describes the asynchronous execution of autonomous actions of the form ∈ ∖{set } by any agent of the pool. Note that such actions do not change the knowledge structure, which is modeled by the set of accessibility relations and by the truth assignment .
The rule (set ) describes the asynchronous execution of autonomous actions of the form set (, ) by any agent , whose side efect is that the truth assignment associated with the current tuple is updated according to the assignment = (see the definition of ′). The accessibility relations are also updated accordingly. On the one hand, the agent performing the assignment acquires knowledge (if not yet possessed) of . Hence, in , all the possible worlds difering for the valuation of (see function dif ) cannot be mutually accessible anymore, as they are distinguishable by the value of . Note that, as we will show, such suppression of connections ensures that the accessibility relation remains an equivalence. On the other hand, all the other agents ̸= lose knowledge (if previously possessed) of , as the assignment is not considered public (as emphasized by the fact that the resulting action is a silent action ). Therefore, in each accessibility relation of those agents, all the possible worlds difering only for the valuation of must become mutually accessible, as they cannot be distinguished anymore. Note that such addition of connections considers the symmetric pairs and, through the closure operation, the transitive relations, thus ensuring, as we will show, that the accessibility relation remains an equivalence.
The most interesting rule is (com), which expresses a communication from an output to a corresponding input (the two actions refer to the same action name ). The agent performing the output and the agent performing the corresponding input synchronize, i.e., they both advance simultaneously. However, the resulting synchronization is enabled only if the epistemic formula communicated from to is known by . If this is the case, acquires knowledge of , and the accessibility relation is updated accordingly. In fact, agent becomes able to distinguish those possible worlds that difer from each other for the evaluation of . The communication is private (the synchronization result is a silent action ), i.e., the knowledge transfer involves only the agent and no one else.
Lemma 1. The KLTS modeling the behavior of a pool of agents is image-finite.
This result immediately derives by Definition 9 and the semantics of Table 2. As anticipated, another important result is that the semantics of Table 2 preserves the indistinguishability interpretation of the accessibility relations.
Theorem 2. Let := (∪ℐ, ∪, ) be a pool of agents such that each , with ∈ , is a P-relation (for P in {reflexive, symmetric, transitive}) and ((, , ∪, ), ) be the semantics of . Then, for each ∈ and for each ∈ , it holds that () is a P-relation.
The present case study is designed to highlight the modeling features and analysis opportunities of our framework. Despite its simplicity, this use case encompasses many of the features of real-world applications, including strategic thinking, private and public communications, and knowledge transfer. For the sake of brevity, instead of the full Cluedo game2 we model a simplified version. Let us consider a game set with 3 players, a dealer, and 8 cards, numbered from 1 to 8. At the beginning of the game, the dealer samples secretly and puts aside two cards, shufles the remaining cards together, making sure none of the cards are seen by any of the players, and then deals two cards per player. Then, the game starts and proceeds by sequential turns. On her turn, each player makes publicly a suggestion of the form: I suggest that the two secret cards of the dealer are and . There are no constraints about the specific choice of and . Then, if the player on the right of the one making the suggestion has at least one of the cards mentioned, she must show one of these cards secretly to her. Then, the inquiry passes to the player on the left, with the same rule. At the end of her turn, the player wins the game if she has learned and can correctly declare what the dealer’s cards are. Otherwise, the game proceeds with the following turns until one of the players wins.
Formally, we model the game set through the propositions and , for 0 ≤ ≤ 2 and 1 ≤ ≤ 8, where means that player has card and means that card is one of the two secret cards of the dealer. The pool includes one dealer and three players and, initially, is defined as the tuple: ({⟨Mr. Black, Dealer ⟩, ⟨0, Player (0)⟩, ⟨1, Player (1)⟩, ⟨2, Player (2)⟩}, , ). The three players have the same behavioral pattern, given by the process term Player , which is fed with a parameter representing the player identity. Set is empty (the cards have yet to be shufled by the dealer Mr. Black - hence all the propositions are set to 0). The accessibility relation of the dealer, Mr.Black , contains only the reflexive pairs, i.e., each possible world is a singleton. In fact, by assumption, the dealer is like an oracle and can distinguish any possible scenario. As we will see, Mr.Black is immutable. The accessibility relation for each player , denoted , is such that two possible worlds are related if and only if they coincide for the values of the propositions , 1 ≤ ≤ 8. The intuition is that, at least, a player is able to distinguish two possible worlds difering in the values of the cards she receives. All such accessibility relations are equivalence relations but are not immutable, as the knowledge of the players will change as the game proceeds.
Initially, the dealer shufles the cards and chooses nondeterministically the two secret cards and the assignments for the players (see actions set):
Dealer := ∑︀1,2 set (1 , 1).set (2 , 1).Deal (1, 2) Deal (, ) := ∑︀1,2̸∈{,} set (01 , 1).set (02 , 1).deal (0, 01 ∧ 02 ).( ∑︀3,4̸∈{1,2,,} set (13 , 1).set (14 , 1).deal (1, 1 3 ∧ 14 ).( ∑︀5,6̸∈{1,...,4,,} set (25 , 1).set (26 , 1).deal (2, 25 ∧ 26 ).Play (0 ))) Whenever clear from the context, the bounds of a summation are not specified (in general, ∑︀, expresses a choice over all the possible unordered pairs of diferent values (, ), each one ranging from 1 to 8). Process term Dealer models the random sampling of the two secret cards, and then the invocation of process term Deal (1, 2) describes the following behavior of the dealer whenever 1 and 2 have been chosen. The sampling for each player is modeled analogously through a pair of subsequent actions set . The output action deal is used to communicate the assignments to the players. Then, the dealer coordinates the game rounds:
Play (x ) := start _turn(, ⊤).(end _turn(_, _).Play ((x + 1 )mod 3 ) + win(_, _).0) 2The reader interested in reviewing the rules of the game can refer to the oficial instructions by Hasbro. by assigning each turn (through the output action start _turn) to a diferent player, sequentially. Note that the output is sent to player to inform that her turn is starting, without the need to communicate any other information (this justifies the choice of the truth constant ⊤). Then, the dealer waits for a response: either the player turn terminates (input action end _turn) or the player wins the game by learning the secret pair during her turn (input action win). For the sake of convenience, whenever unnecessary, the arguments of an input action are left unspecified (symbol _).
After receiving the cards through the input action deal , each player is available to start her turn (input action start _turn) or to manage inputs from the other players. The process term Player () is defined as follows:
Player () := deal (, _).
(start _turn(_, _). ∑︀1,2 ask 1,2 (( + 1)mod 3, ⊤).show (_, _).
ask 1,2 (( + 2)mod 3, ⊤).show (_, _).
(end _turn(, ¬).Player () + win(, ).0)) + ∑︀1,2 ask 1,2 (, _).
(show (3 − − , 1 ∨ 2 ).(show (, 1 ).Player () +
show (, 2 ).Player ()) + show (3 − − , ¬1 ∧ ¬2 ).show (, ¬1 ∧ ¬2 ).Player ()) +show (_, _).Player ()) When initiating a new turn, the player chooses nondeterministically two cards to be asked to each other player (output action ask) and then waits for the related answer (input action show). At the end of the turn, either the player learns the secret and wins the game (output action win) or passes the hand (output action end _turn). The winning condition for player determining which output is executed is given by the knowledge of the formula = ⋁︀(,′) ( ∧ ′ ), i.e., the player knows the secret pair. Then, players respond to incoming requests through the input action ask. If player receives from player a request about cards 1 and 2, then we distinguish two cases. Firstly, may have at least one of the two cards (1 ∨ 2 ). In this case, reveals one of the possessed cards to , by choosing the card nondeterministically if necessary. Indirectly, even the third, silent player (identified by 3 − − ) learns something, i.e., the fact that has one of the two cards. We model this indirect transfer of knowledge through an explicit output directed to player 3 − − . Secondly, may have none of the two cards (¬1 ∧ ¬2
). In this case, the information is shared with both the other players. Finally, due to the outputs directed to player 3 − − , players must also be available to learn some information during the turns of the other players (through the input action show ).
It is worth noting that the management of the knowledge base of the players is left to the
semantics of the underlying Kripke model. At the level of the specification, only the initial
setting and the communications are modeled explicitly. This is particularly significant from the
viewpoint of usability, as an analogous model based on, e.g., classical Kripke structures, would
be much more challenging. To appreciate this aspect, the same use case has been modeled in
the software tool NuSMV [
To show an example of properties that can be model checked, we consider the derived eventually modality , such that , |= if and only if , |= or ∃. , |= ⟨ ⟩ , and the derived globally modality , such that , |= if and only if , |= and ∃. , |= ⟨ ⟩. Then, the reachability property (⋁︀ ) is satisfied, i.e., the winning state is reachable by some players. However, even the unreachability property (⋀︀ ¬) holds. The reason is that the simple, nondeterministic strategy followed by the players when choosing their suggestion does not guarantee that the game can always be won.
A few approaches investigate the combination of LTS-based semantics and epistemic notions,
e.g., in the setting of epistemic -calculus [
An important strand of research concerns dynamic extensions of Kripke models and epistemic
logic, where the dynamic dimension is related to the execution of actions over time; see, e.g.,
[
In the field of concurrency theory, some of the ideas presented in this paper can be found
in the study of temporal logics encompassing features from HML and modal -calculus [
Summarizing, by following suggestions deriving from works on dynamic and temporal
epistemic logics [
Starting from this point, several extensions can be envisioned. For instance, the semantics
of our communication mechanisms assumes that only known truth can be transferred. Hence,
we do not currently manage (possibly false) beliefs and the communication of information
that is inconsistent with an agent’s knowledge or belief. This would require the introduction
of the belief modality and the treatment of contradictions resulting from the communication
between agents. Moreover, this would also open to extensions in which it is possible to model
the behavior of malicious agents sharing false information and, therefore, a theory of fake news
[
Dealing with inconsistencies is a problem to face even in the present model, without bringing up the notion of belief. In particular, an unsuccessful formula is a formula that might become false as soon as it is communicated, like, e.g., in the case of ∧ ¬ whenever agent communicates it to agent [37]. Several studies investigate the syntactic form of potential unsuccessful formulas, in particular in the setting of public announcements for multi-agent systems [38]. Obviously, even in our framework such forms can be recognized and, in particular, are limited to those cases in which a formula of the form ¬ is involved in a communication to agent . This is because the satisfaction of ¬ before the communication could be contradicted by sharing its knowledge with the agent sufering from such a kind of ignorance. The formal investigation of these situations is left as future work.
Given the high generality of the proposed framework, it would also be interesting to investigate the relation with other abstract models, such as coalgebraic modal logics [39], to better guide the comparison with the literature. Finally, we also plan to define: () an axiomatization for the KT logic, () quantitative extensions of the KLTS model, by adding continuous time and probabilistic choices, and () additional ingredients in the process-algebraic language, by including internal actions guarded by knowledge-based requirements, if-then-else constructs that are based on knowledge conditions, asynchronous communication and dynamic pools of agents, broadcast communication in the style of [40]. [36] A. Aldini, G. Curzi, P. Graziani, M. Tagliaferri, A probabilistic modal logic for contextaware trust based on evidence, International Journal of Approximate Reasoning 169 (2024) 109167. [37] H. Van Ditmarsch, B. Kooi, The secret of my success, Synthese 151 (2006) 201–232. [38] S. Saraf, S. Sourabh, Characterizing successful formulas: the multi-agent case, CoRR abs/1209.0935 (2012). [39] C. Kupke, D. Pattinson, Coalgebraic semantics of modal logics: An overview, Theoretical
Computer Science 412 (2011) 5070–5094. [40] A. Aldini, Design and verification of trusted collective adaptive systems, Transactions on Modeling and Computer Simulation (TOMACS) 28 (2018).