THE LABELED GRAPH ASSOCIATED TO A TRANSITION SYSTEM [600276]

THE LABELED GRAPH ASSOCIATED TO A TRANSITION SYSTEM
Beatrice Daniela BUCUR1
Abstract
The aim of this paper is to establish a connection between modal logics and la-
beled graphs, which is useful in solving the problem of undeterminism. Further, we
construct a canonical, maximal and consistent model of a labeled graph associated to
a transition system.
2000 Mathematics Subject Classication: 03B45, 03C80, 05C78.
Key words: labeled graph, transition system, undeterminism, consistency.
1 Introduction
The most famous theories about modal logic are based on the model built by Saul
Kripke which, in a restricted sense, refers to necessity and possibility.
The semantics of modal logics consists of a non-empty set G;whose elements are called
possible worlds, a binary relation Rbetween the elements of Gcalled accessibility relation
and a labeling function which describes every situation. Modal logic makes use of the
modal operators (necessary) and (possible), see, e.g., [3].
Denition 1 ([3]).A Kripke model is a tuple (S; R; L )where Sis a set of states (possible
worlds), Ran accessibility (transition) relation with RSSsuch that8s12S9s22S
with (s1; s2)2RandL:S!2APa labeling function such that 8s2S; L(s)represents
all the atomic propositions true in sandAPis the set of atomic propositions.
2 Transition systems
Transition systems are concepts used in computer science. They consist of states and
transitions among them. The set of states can be countable or uncountable, and so can
the set of transitions.
Denition 2 ([1]).Formally, a transition system STis a triple (S; A;!);where Sis a
set of states, Aa set of actions and !SASis the transition relation.
We can consider the transition system ST;a tuple ( S; A;!; P; L ) where Sis a set
of states, Aa set of actions, !SASis a transition relation, Pa set of atomic
propositions and L:S!2Pa label function.
To a transition system we can associate a set of atomic propositions which depend on
the properties taken into account. Thus we can obtain a variety of choices which a logical
analysis is able to predict. From the point of view of transition mechanisms, the choice is
arbitrary.
1Department of Computer Science, University of Pite sti, Romania, e-mail: ciolan [anonimizat]

2 Beatrice Daniela Bucur
3 Undeterminism
What is important for modeling transition systems is the undeterminism, which is more
than a theoretical concept. It allows for freedom in modeling the computation systems.
Intuitively, a transition system begins with an initial state and evolves to another state
according to the accessibility relation. If from one state there can be more transitions,
then the choice of the next state is undeterministic. That is, the result of the selection is
not a priori known, therefore one can draw no conclusion regarding the probability with
which a certain transition is chosen. The same aspect is met also in the case when there is
not only one state, but a set of initial states, in which case the undeterministic factor plays
a role. The analysis of these choices is useful in modeling con
ict situations which may
appear in case of processes executed in parallel, but also in modeling unknown interfaces
(see [2]).
However, it is useful to take into account the observable, deterministic behavior, related
to various observable notions. In this way, the determinism agrees with the executable
actions which are observable, or it is related to labels and relies only on the atomic
propositions which take place and are observable. To simplify, the atomic propositions of
the system are statements on which the binary operation yes/no acts. If the names of the
actions are not relevant, as transition represents an internal process, we can use symbols,
or even omit them in certain cases.
4 Labeled graphs
Denition 3 ([4]).A labeled graph is a tuple LG= (S; E; T; f )where Sis a nite set of
elements representing the vertices of LG; E is a set of elements used to label the edges of
the graph, Tis a set of binary relations on Sandf:E!Ta surjective function.
Remark 1. In the graphical representation of this structure, the vertices are drawn as
boxes which contain their names. An edge from xi2Stoxj2Sis labeled by a2Eif
and only if (xi; xj)2f(a):
5 Labeled graphs and transition systems
We notice the following:
1. A labeled graph can be interpreted as a transition system.
2. The states of STare the vertices of the graph.
3. The actions of STcan be associated with the labels of the graph.
We dene the labeled graph associated to a transition system, and denote this by
LG(ST);to be a tuple ( S; E; T; f );where Sis the set of states, Ethe set of actions, T
the set of atomic propositions and f:E!Ta surjective function.

The labeled graph associated to a transition system 3
Denition 4. A model Mis a tuple M= (S; T; f )where Sis a set of states, Tis a
binary relation and f:E7!Tis a function which assigns to an action, a2E;a subset
of states from S;namely those states for which ais true.
Denition 5. An action is true in a model Mif the following conditions are satised:
1.(M; x 1)a8x12f(a):
2.(M; x 1):aif and only if (M; x 1)6a:
3.(M; x 1)a^bif and only if (M; x 1)aand(M; x 1)b:
4.(M; x 1)a_bif and only if (M; x 1)aor(M; x 1)b:
5.(M; x 1)a!bif and only if (M; x 1)6aor(M; x 1)b:
6.(M; x 1) aif and only if8x22Swithx1Tx2we have (M; x 2)a:
7.(M; x 1) aif and only if9x22Swithx1Tx2and(M; x 2)a:
The above denition allows us to introduce the concept of a valid action in a model
M= (S; T; f ):
Denition 6. An action ais valid if it is true for any state xi2S;taht is, Maif and
only if (M; x i)a8xi2M:
Denition 7. A frameworkCis a pairC= (S; T)consisting of a set of states and a
binary relation on that set. If M= (S; T; f ) = (C; f);we say that Mis based on the
frameworkCandCis the framework of M:
Using the concept of framework, we can extend the denition of a valid action, by
saying that an action ais valid in a framework Cif (M; x)afor every model Mbased
onCand every x2M:
Denition 8. An action aisMprovable if it arises as the last element of some Mvalid
actions and we denote this by `Ma:
We say that a labeled graph LG(ST) associated to a transition system is valid with
respect to a class Kof frameworks if every provable action is valid. That is, if P`La
then PCafor everyC2Kand if ( M; x)Pthen ( M; x)afor all x2S:(We used L
to denote LG(ST):)
Denition 9. A labeled graph associated to a transition system is complete if every valid
action is provable.
The notions of correctness and completeness are relative and refer to a certain class of
frameworks.
To prove the completeness, we will construct, for every L;a canonical model with
the property of \validating" all provable actions. The existence of such a model is a
consequence of the fact that Lis complete with regards to its model.

4 Beatrice Daniela Bucur
Denition 10. An action ais consistent if6`L:a:
Denition 11. A set is Lconsistent if there exists no P0P; P0=fa1: : : a ngsuch
that`L:(a1^: : :^an).
Denition 12. A set of atomic propositions PisLconsistent if P`La:
Denition 13. A set PisLmaximal if P[fagisLconsistent for every a62P:
Starting with an Lconsistent set, Lindenbaum's lemma will allow us to nd a maximal
Lconsistent set. According to this lemma, if Pis a set of atomic propositions, then there
is a set Rsuch that Ris maximal, Lconsistent and PR:
6 Conclusions
The consistency of an LG(ST) depends on the interpretations proposed for it. The
consistency implies the fact that an action becomes valid when it is interpreted.
Our future endeavors will deal with proving that every maximal Lconsistent set P
is complete with regards to negation.
References
[1] C. Baier and J.-P. Katoen, Principles of model checking , The MIT Press Cambridge,
London, 2008.
[2] P. Blackburn and J. van Benthem, Modal logic: a semantic perspective , 2010.
[3] S. Kripke, Semantical considerations on modal logic , 1963.
[4] N. Tandareanu, Baze de cunostinte , Universitatea din Craiova, 2004.