Populational Announcement Logic (PPAL), is a variant of the standard Public Announcement Logic (PAL) with a fuzzy semantics, where instead of specific agents we have populations and groups. The semantics and the announcement logic are defined, and an example is provided. We briefly talk about decidability and model checking. We conclude that the main advantage of PPAL over DEL and PAL is the flexibility to work with non-priorly defined agents.
Epistemic logics attempt to provide ways to reason about knowledge representation models [ ]. C. I. Lewis published back in the book “Survey of Symbolic Logic”, possibly the first systematic approach to the matter [ ].
Later in , Von Wright’s “An Essay in Modal Logic” introduced a concept called “modality” to better represent the semantics of knowledge [ ], providing operators such as “usually” and “always” to qualify propositional statements. It is considered the first important work regarding modal logic.
A further development is Dynamic Logic, which reasons about actions and their effects [ ]. Dynamic Epistemic Logic (DEL) is conceived to reason about actions that change agents’ knowledge and beliefs. It is not interested in justifying whether something is knowledge or not, but in inferring something from said knowledge.
The first Dynamic Epistemic Logic was proposed independently by [ ] and [ ], and is called Public Announcement Logic (PAL), a logic which allows simple public actions which alter the state of knowledge for its agents. Later [ , ] proposed the Action Model Logic approach, allowing for more complex reasoning.
This work aims to specify a variation of PAL where knowledge is represented across populations and groups of populations, instead of discrete agents as it is normally done. The motivation behind this is to provide a framework that is capable of dealing with applications where one intends to reason about evolution of knowledge across populations instead of individual agents. It is specially designed for model checking, because it is not necessary to specify agents (or populations in this case) beforehand, and instead these populations can be defined in the middle of the execution by the announcement operators of the language.
To achieve this we have introduced and defined a “fuzzyfied” variant of PAL that allows partial announcements to its agents (called “populations” and “groups”). We formalize the model, language and semantics, and give an example where an initial model is given and some announcements are made which modify it, in order to illustrate its applicability in a scenario where knowledge evolves across populations as announcements are made. .
In section we introduce Public Announcement Logic (PAL), showing a classical example to illustrate its use. In section , we introduce Populational Announcement Logic (PPAL), explain its purpose and differences with respect to PAL and define its language, semantics and model. We also talk about decidability and a model checker. Section provides two basic examples of PPAL, showing how the model evolves after an announcement. Section provides a conclusion, some final remarks and future works.
Public Announcement Logic (PAL) Now, we will briefly introduce the Public Announcement Logic, an extension to Multi-Agent Epistemic Logic which has been investigated in Computer Science [ ] to represent and reason about agents or groups of agents’ knowledge and beliefs. It is the first actual Dynamic Epistemic Logic, developed by Plaza in [ ]. where ∈ , the set of countably many proposition symbols, and ∈ , a finite set of agents. The operators ∨ and → can be derived from the others similarly to propositional logic.
The modal operator of public announcement [ ] has the intended meaning: “after the announcement of , holds”. The effect of announcing publicly is a restriction in the model to contain only states where is true.
Definition Given a multi-agent epistemic model ℳ of satisfaction ℳ , |= is defined as follows: = ⟨, ∼ , ⟩, the notion – ℳ , |= iff ∈ ( ) – ℳ , |= ¬ iff ℳ , ̸|= – ℳ , |= ∧ iff ℳ , |= and ℳ , |= – ℳ , |= iff ∀ ′ ∈ : ∼ ′ ⇒ ℳ , ′ |= – ℳ , |= [ ] iff ℳ , |= ⇒ ℳ| , |=
where ℳ| is a new model obtained by restricting ℳ where holds. to have only states This example is from [ ]. Suppose we have a card game with three cards: 0, 1 and 2, and three players , and . Each player receives a card and does not know the other players cards. We use proposition symbols 0 , 1 , 2 for ∈ {, , } meaning “player has card 0, 1 or 2”. We name each state by the cards that each player has in that state, for instance 012 is the state where player has card 0, player has card 1 and player has card 2. Figure shows the epistemic model 1 which represents the epistemic state of each agent. 102 c b 012 a 021 c
b 201 a 210 b c a
120
We are now going to make a public announcement and check the knowledge of an agent after that. Consider an announcement that agent does not have card 1 (¬1 ), and after that we want to check if agent knows if agent has the card 0 ( 0 ). This can be expressed as:
1, 012 |= [¬1 ] 0
The epistemic model 2 representing the epistemic state of each agent after the announcement is shown in figure .
We can check if 0 holds in the new model 2: 2, 012 |= 0
2, 012 |= 0
Now, we have to check if 0 is true in every state connected to state 012 via the relation ∼ . Since there are no other states other than 012 itself, we check only this state:
Which is true because 012 ∈ ′(0 ), and therefore true. 2, 012 |= 0 is also ( ) ( ) ( ) 012 a 021 c
b 201 a 210 Now we introduce PPAL, where we have populations and groups instead of agents. It works like a “fuzzyfied” version of PAL, where announcements act upon fractions of populations, so it does not make sense to talk explicitly of private or public announcements. It should be noticed that in the limit case where announcements are made to the whole population, PPAL behaves similarly to PAL with public announcements.
This allows us much more flexibility, as we can define the populations of the system beforehand. Also, it allows expressing partial knowledge in a much more natural way.
As a motivation, consider the following example: A famous politician is under suspicion of money laundering and bribery. Elections are coming up, and this politician expects to be re-elected, but people are less willing to vote for him if they are aware of both charges against him. Not everyone in the population is aware of the charges, however. With PPAL we can model announcements made by a TV program which only a certain amount of the population sees, and then we can assert the overall knowledge of the population in regards to the politician. For instance, the formula [ ]0.3 ( ∧ ) ( ) represents an announcement made to a fraction of 0.3 of a group , that the politician is in fact guilty of money laundering ( ), and a subsequent knowledge assertion of whether knows that the politician is corrupt or not (guilty of money laundering and bribery).
We will return to this example in section .
It is defined as a real number because announcements split populations into a group with two populations, and their sizes will be then fractions of the population’s size.
Note that while a population represents many individuals, actual individuals are never directly expressed or referenced (as in DEL). Individuals are represented solely by the size of the population. The motivation for this comes down to the fact that we are mostly interested in representing and working with the knowledge of populations or fractions of populations, thus there is no purpose in modelling actual individuals. Next we will define the notion of groups.
A group can be empty, a population or a disjoint set of groups: := ∅ | | { 0, 1, . . . , } ( ) The size of a group is defined as: = ⎧ 0 ⎨ if if ⎩ ∑︀ ∈ if = ∅, = , = { 0, 1, . . . , }.
The reason for having two definitions for “groups” and “populations” is the fact that announcements operate splitting groups into populations, as will be seen in section . and in subsection . Having groups and populations allows for a clearer definition of announcements, because if we only had populations there would be no easy way to reference, as a whole, the same individuals that we could reference before the announcement was made and they were a single population. Since the announcements apply to fractions of a population, they work similarly to private announcements. Due to this, the many worlds approach is used. Each population has its own model, representing its current knowledge of the world: Definition A model for a population , = ⟨, ∼, , ⟩ is composed of a set of states , a valuation function that maps propositional symbols in into subsets of , : → 2 , and a family of binary relations over , ∼, . For example, an edge representing the doubts of population in regards to group would be in the relation ∼, .
Definition A model , for a group = { 0, 1, . . . , } is defined as the set of models of each of its groups. That is, = { 0 , 1 , . . . , }.
Since announcements split groups into populations, groups appearing on a branch after a split are not known to groups on other branches. That is, they will not appear on these groups’ models. . Language
: “ 2 is true on group ’s model after the announcement of 1 to fraction of the individuals in ”, where This expression describes a partial announcement which defines two new populations, one of them with additional knowledge announced and other that did not received the new information announced. = { 1, 2} and 1 = .
. Semantics This section presents the semantics of PPAL. We start by redefining (fuzzifying) the valuation functions defined in
and . In order to achieve that, we define an evaluation function : × ( , ) → where ∈ , is a model for , is a state and is the unit interval [0, 1]. We can define the semantics as follows: , ( ) = (, ( , )) , (¬ ) = , ( ∧ ) = , ( ∨ ) = , ( → ) = ( , ( )) ( , ( ), , ( )) ( , ( ), , ( ))
( , ( ), , ( )) , ( ′ ) = (, ( , ), ′) , ( ′ ) = (, ( , ), ′) , ([ ] ) = , ( ) where ¬
where ∃ 1, 2 such that that 1 = | and 2 = | = { 1, 2}, and 1− . ⊤ is a symbol for | is defined as the new mod⊤el obtained from holds, and multiplying all the sizes inside it by .
.
= { 1, 2} such by removing all states
Depending on the choice of the evaluation function we can have different semantics. One possible evaluation function is the crisp evaluation. Suppose = ⟨, , ′, ⟩ ∼ (, ( , )) = 1 if ∈ ( ) , and 0 otherwise ( ) Below, we give some properties about the fuzzy functions that are used in the definition of satisfaction. At this point we choose not to define a particular fuzzy semantics and instead define classes for each operation. One can choose any
– (0) = 1; – (1) = 0; – ≤ → ( ) ≤ ( ).
A binary operation – (, ) = – (, – ≤ → – (, 1) = .
(, ); (, )) = (, ) ≤ :
→ is a fuzzy negation if : 2 → is a fuzzy conjunction if ( (, );
(, ), ); semantics which satisfies the following properties, and we provide an example for each of the classes.
It is also important to note that this work is concerned with model checking and for that the notion of satisfaction is enough. For this reason we did not define the consequence relation.
For instance, a possible negation function is ( ) = 1 − .
– (, ) = (, ); – (, (, )) = – ≤ → (, ) ≤ – (, 0) = .
Fuzzy Implication – ≤ → (, ) ≥ – ≥ → (, ) ≥ – (0, ) = 1; – (, 1) = 1; – (1, 0) = 0.
(
(, ), ); (, ); (, ); (, );
For instance, a possible implication function is also known as the Łukasiewicz implication. (, ) = {1, 1 − + }, These also define precisely the class of t-norm functions, which are widely used in fuzzy logics as they are considered “well-behaved” functions [ ]. For instance, a possible conjunction function is (, ) = {, }.
: 2 → is a fuzzy disjunction if These also define precisely the class of t-conorm functions, analogous to the t-norm class. For instance, a possible disjunction function is (, ) = {, }.
: 2 → is a fuzzy implication if . Fuzzy Knowledge Assertion A ternary operation : × ( , ) × → is a fuzzy knowledge assertion if – if = then ∀ ′ ∈ | ∼, ′[ , ′( ) = 1 → (, ( , ), ) = 1]; – if = then ∀ ′ ∈ | ∼, ′[ , ′(¬ ) = 1 → (, ( , ), ) = 0]; – (, ( , ), ) ≤ ′∈ { (, ( , ), ′)}; – (, ( , ), ) ≥ ′∈ { (, ( , ), ′)}.
For instance, a possible knowledge assertion function is (, ( , ), ) = ⎪⎨⎧ ∑︀ ′∈ ′ (, ( , ), ′) if ̸= , if ∀ ′ ∈ | ∼, ′ → , ′( ), otherwise.
Note here that we slightly abuse notation for binary relations when they appear referring to models of groups, such as the expression ∼, , which represents the binary relation for the model of population contained inside .
Intuitively, it means that the knowledge of a group is equal to the weighted average knowledge of its contained groups, is equal to 1 when the group is a single population and is true in every state connected to state via , , and ∼ 0 otherwise. A single population knows something only when it is true in every conceivable world this population contemplates. A ternary operation : × ( , ) × → is a fuzzy belief assertion if – if = then ∃ ′ ∈ | ∼, ′[ , ′( ) = 1 → (, ( , ), ) > 0]; – if = then ∃ ′ ∈ | ∼, ′[ , ′(¬ ) = 1 → (, ( , ), ) < 1]; – if = then ∀ ′ ∈ | ∼, ′[ , ′( ) = 1 →
(, ( , ), ) = (, ( , ), )]; – (, ( , ), ) ≤ ′∈ { (, ( , ), ′)}; – (, ( , ), ) ≥ ′∈ { (, ( , ), ′)}.
For instance, a possible population belief assertion function is (, ( , ), ) =
︀∑ ′∈ ⎪⎩ 0 ⎪⎧⎨ ∑︀ ′∈ , ′( ) ′ (, ( , ), ′) if ̸= , if ̸= ∅, otherwise. where = ⋃︀ ′∈ | ∼, ′ ′ are the neighbours of via relation ∼, .
Which is functionally similar to , but allowing any number in the interval [0, 1]. For example, if in half of the states connected to state via , , ∼ evaluates to 1 and in the other half to 0, then (, ( , ), ) = 0, 5. And also similarly to , the belief of a group is equal to the weighted average beliefs of its contained groups. An important aspect of model checking a logical system is that of decidability. In this section we show that any valid finite formula of the PPAL language over a finite model is in fact decidable. We use induction over the size of the formula for this proof.
The size for each expression of the language is defined as follows: – ( ) = 1; – ( 1 ∧ 2) = ( 1 ∨ 2) = ( 1 → 2) = ( 1) + ( 2) + 1; – ( ) = ( ) = ( ) + 1 + | |; – ([ 1 2) = ( 1) + ( 2) + 1 + | |.
]
Next, we can proceed to the induction basis step where = 1, that is, the case of a formula consisting of a single propositional symbol. , ( ) = (, ( , )) evaluates to 1 or 0 in a finite model, and therefore is decidable.
We then consider the induction hypothesis to be that any formula with size is decidable. Now it remains necessary to take the inductive step, assuming the induction hypothesis and proving that formulas with size + are also decidable, where ∈ R>0. Note that is in the real interval because the size | | of a group can be a real value.
Inductive step: . , (¬ ) = NOT ( , ( )): NOT is a simple mathematical function which evaluates to a value in for any input in . Since , ( ) is decidable by hypothesis, this formula is decidable. , ( ∧ ), , ( ∨ ) and , ( → ) are all decidable due to the same arguments; . , ( ′ ) = K (, ( , ), ′): (a) It is trivially decidable when ′ = ∅, because its evaluation will always be equal to 0; (b) It is decidable when ′ = , as the formula is resolved via calculations of , ′ ( ) which is decidable by hypothesis; (c) In the case where ′ = { ′0, ′1, . . . , ′ }, the sum will range recursively over every ′ ∈ ′. The sizes | ′ | are strictly smaller than | | because by definition the group ′ is composed of a disjoint set of groups. Due to this, ( ′ ) < ( ′ ) and ′ is decidable by hypothesis. ′ is resolved via calculations of ′ , therefore, the formula is decidable. . , ( ′ ) = B(, ( , ), ′): (a) It is trivially decidable when ′ = ∅, because its evaluation will always be equal to 0; (b) When ′ = , the sum ranges over all neighbours ′ of state , but since the model is finite and , ′ ( ) is decidable by hypothesis, it is decidable; (c) In the case where ′ = { ′0, ′1, . . . , ′ }, the same argument used in b shows this formula is decidable. . , ([ ] ′ ) = ′ , ( ): is finite and therefore ′ is also finite as it contains exactly twice the number of elements in . To define ′ we need to calculate , ( ) for every ∈ , which are decidable by hypothesis. ′ , ( ) is also decidable by hypothesis. Also note that it is not possible to write a formula that divides the group indefinitely, as that would require us to write down an infinite number of announcements. Therefore, the formula is decidable.
Hence we have covered every possible case and shown that they are all decidable, therefore successfully showing that any valid finite formula of the PPAL language over a finite model is decidable using the specified operator functions.
Notice however, that recursive formulas such as := [ ] ′ or := [ ] ′ are not included in the language definition, and they would break the language’s property of being decidable. A general-purpose Java library implementing the aforementioned language and semantics, and a model checker have been developed. Both programs are covered by unit and integration testing to ensure consistency with the PPAL language and semantics. The source-code of both library and model checker are available on GitHub .
The main current implementations of model checkers available for epistemic logics are MCK [ ], MCMAS [ ] and DEMO [ ]. A recent development called SMCDEL [ ] formalizes a new structure to represent DEL models which allows for symbolic model checking, a model which uses binary decision diagrams (BDDs) [ ] to represent models instead of having every state directly represented in the system. Due to this, SMCDEL also provides better performance over the other model checkers.
In this section we continue the example introduced in section , where a simple model is established and some assertions are made to probe the knowledge represented by this model. For clarity’s sake, we name the states with the set of propositional symbols, or their negation, that hold in it. For instance, state {, ¬ } is the state where and ¬ are true. Also, we will omit the full math for some of the simplest equations due to space constraints.
https://github.com/vittau/PPAL .
Suppose an initial model composed of a single population with size = 1, two propositions (money laundering) and (bribery), and a real state = {, }, which means the politician in fact is guilty of the charges against him. The evaluation function is the same as defined before. This model is as shown in figure .
,
, ( ( )) much of the population would not vote on the politician, that is, if we ask: For brevity, let us call = ∧ here onwards. As expected if we assert how It will evaluate to 0, as there are edges connecting the state to other states. Then, a TV program aired revealing the politician in fact did money laundering, but given that only 30% of the population watched the program, only a fraction of the population is now aware of this fact. This is equivalent to the announcement [ ]0.3, where = { 1, 2
} is a group containing the two populations resulting from the announcement: 1 who received the announcement, and 2 who did not. Figure
shows the resultant model G.
If we were now to assert how much of the population would not vote on the politician, we would be asking: , ([ ]0.3
( ))
The announcement [ ]0.3 generates group , which contains populations 1 and 2, where the former received the announcement. ( ) will still evaluate to 0, as there are still 1 and 2 edges connecting the state to other states. That is, both populations remain in doubt about whether is the real state or not. ( ) ( ) ¬, ( ) ( )
We could also make an assertion in regards to the belief of the population, that is:
, ([ ]0.3 ( )) To evaluate the belief we must evaluate , ( ( )), which expands into
The first sum evaluates to 1/2 because out of two neighbour states to ({, } itself and {, ¬ }), is only true in . The second has all four states as neighbours, but is only true in again. The result 0.325 demonstrates a small belief at this moment that the politician is in fact corrupt. Now, let us consider another TV program aired, and this time covering 40% of the same original population, and it was told that the politician is in fact guilty of bribery. This corresponds to the announcement [ ]0.′4, where ′ = { 1, 2} is a group containing the two groups resulting from the announcement: 1 who received the announcement, and 2 who did not. The model resulting from both announcements is shown in figure .
If we were now to assert how much of the population would not vote on the politician, we would be asking: , ([ ]0.3[ ]0.′4 ′ ( )) ( )
At this moment the assertion would evaluate to 0.12, since there are no more edges connecting the state to anything else for population 11 in 1.
This example shows how pieces of knowledge can build up to create useful information for certain fractions of the populations, due to them having being exposed enough to these pieces, and how it might not be intuitive to find out how much exactly of a population knows a certain fact. ¬, ,
Final Remarks, Future Works and Acknowledgments In this work we introduced and defined a “fuzzyfied” variant of PAL that allows partial announcements to its populations.
The main advantage of PPAL over DEL and PAL is the flexibility to work with non-priorly defined agents. It is possible to define an initial population and have it evolve in a more natural way that doesn’t require a formal initial definition of every agent on the system. Therefore we believe it can be a more appropriate logic for practical use, as it would be much easier to manage a knowledge model.
We also believe this work expands horizons for the definition of “dynamic” logic, as not only accessibility relations are dynamic, but the agents of the world themselves are changing and evolving. As such, it is a worthwhile topic of theoretical discussion, and not only of interest for model checking applications. There is room for further development on a few directions still, and one important formalism for logics is that of axiomatization, that is, a set of tautologies (formulas that are always true in the logic), called axioms in this case, that can be used to derive all other formulas in the language.
We did not attempt symbolic model checking, a way to represent all reachable states using only sets of states and formulas for transition relations, which can improve performance. One such approach is based on the previously mentioned BDDs, which provide a compact way to represent and check valuations in Boolean functions, and equivalent Boolean sub-expressions are uniquely represented.
We wish to thank the research agencies CNPq, CAPES and FAPERJ for their support.