Exploring paraconsistent logics for quantum programs

Universidade do Minho Escola de Engenharia Departamento de Inform´ atica Ana Luzia Cruz Exploring Paraconsistent Logics for Quantum Programs Paraconsistent transition systems Modal paraconsistent logic December 2021 Universidade do Minho Escola de Engenharia Departamento de Inform´ atica Ana Luzia Cruz Exploring Paraconsistent Logics for Quantum Programs Paraconsistent transition systems Modal paraconsistent logic Master dissertation Integrated Master’s in Physics Engineering Dissertation supervised by Lu´ıs Soares Barbosa Alexandre Madeira December 2021 i DIREITOS DE AUTOR E CONDIC¸ ˜ OES DE UTILIZAC¸ ˜ AO DO TRABALHO POR TERCEIROS Este ´ e um trabalho acad´ emico que pode ser utilizado por terceiros desde que respeitadas as regras e boas pr´ aticas internacionalmente aceites, no que concerne aos direitos de autor e direitos conexos. Assim, o presente trabalho pode ser utilizado nos termos previstos na licenc¸a abaixo indicada. Caso o utilizador necessite de permiss˜ ao para poder fazer um uso do trabalho em condic¸ ˜ oes n˜ ao previstas no licenciamento indicado, dever´ a contactar o autor, atrav´ es do Reposit´ oriUM da Universidade do Minho. https://creativecommons.org/licenses/by/4.0/ ii STATEMENT OF INTEGRITY I hereby declare having conducted this academic work with integrity. I confirm that I have not used plagiarism or any form of undue use of information or falsification of results along the process leading to its elaboration. I further declare that I have fully acknowledged the Code of Ethical Conduct of the University of Minho. ACKNOWLEDGEMENTS I once read that we have no friends, only teachers. I am lucky to have found great teachers who are great friends. I would like to thank professor Alda Pregueiro, professor Rosa Sousa, professor Jos´ e Lopes and all the teachers I had the opportunity to learn with in the last 18 years. Mostly, I would like to thank professor Lu´ ıs Soares Barbosa and professor Alexandre Madeira for leading me through the quest of developing the work here presented, for their suggestions and insights and for their brightness. Knowledge is either a useless or a dangerous thing in the hands of those who don’t know how to share it. Thank you all for sharing your beautiful minds. I would like to thank all my family members and all my friends for always supporting me and heartening me to succeed. No step is the last step. Thank you for witnessing and greeting all my steps, even those which lead me nowhere. ABSTRACT Superconducting quantum circuits are a promising model for quantum computation, although their physical implementation faces some adversities due to the hardly unavoidable decoherence of superconducting quantum bits. This problem may be approached from a formal perspective, using logical reasoning to perform software correctness of programs executed in the non-ideal available hardware. This is the motivation for the work developed in this dissertation, which is ultimately an attempt to use the formalism of transition systems to design logical tools for the engineering of quantum software. A transition system to capture the possibly unexpected behaviors of quantum circuits needs to consider the phenomena of decoherence as a possible error factor. In this way, we propose a new family of transition systems, the Paraconsistent Labelled Transition Systems (PLTS), to describe processes that may behave differently from what is expected when facing specific contexts. System states are connected through transitions which simultaneously characterize the possibility and impossibility of that being the system’s evolution. This kind of formalism may be used to represent processes whose evolution is impossible to be sharply described and, thus, should be able to cope with inconsistencies, as well as with vagueness or missing information. Besides giving the formal definition of PLTS, we establish how they are related under the notions of morphism, simulation, bisimulation and trace equivalence. It is a common practice to combine transition systems through universal constructions, in a suitable category, which forms a basis for a process description language. In this dissertation, we define a category of PLTS and propose a number of constructions to combine them, providing a basis for such a language. Transition systems are usually associated with modal logics which provide a formal setting to express and prove their properties. We also propose a modal logic, more specifically, a modal intuitionistic paraconsistent logic (MIPL), to talk about PLTS and express their properties, studying how the equivalence relations defined for PLTS extend to relations on MIPL models and how the satisfaction of formulas is preserved along related models. Finally, we illustrate how superconducting quantum circuits may be represented by a PLTS and propose the use of PLTS equivalence relations, namely that of trace equivalence, to compare circuit effectiveness. Keywords: Paraconsistency, Transition systems, Modal logic, Quantum computation. list of figures xiii 1 INTRODUCTION Logic for what? Logics are used to study the validity of arguments, or in other words, to verify if a particular statement, the conclusion, may be fairly inferred from a set of other statements, the premises. To do so, it is necessary to define a collection of rules that determines what conclusions follow from the assertion of a number of statements, called a theory. That is, if the information contained in a theory is assumed or known to be true, the logic rules of inference establish what other statements are provable, allowing to derive further truths. The concept of provability needs to be complemented with the notion of truth so that it is possible to make distinction between arguments that are valid, or, in other words, logically provable, and arguments that in addition to being valid also lead to a true conclusion, called plausible arguments. The difference between a conclusion being provable and a conclusion being true is illustrated by the argument below. All computer scientists are logicians. All logicians are mathematicians. Thus, all computer scientists are mathematicians. This argument has the form of a syllogism, a particular kind of argument defined by Aristotle. The last statement, the conclusion, is provable from the previous ones, the premises. Indeed, if the premises are assumed to be true, then the conclusion is necessarily true. However, it is reasonable to question the veracity of the information expressed by the premises, and if at least one of the premises is false then it is no longer possible to ensure the veracity of the conclusion. To distinguish true and false statements, logics are complemented with semantics, whose role is to interpret statements according to their truth value. When logics are enriched with a semantical layer, the veracity of premises, or their truth value, is accounted for in establishing if a conclusion is true or false. Classical logics: when contradiction and triviality are inseparable 2Chapter 1. Introduction Classical logics are a family of logics whose semantics is usually bivalent, meaning that each statement has one of two possible truth values: true or false. Bivalent classical logics obey the Principle of Non-Contradiction. Formulated by Aristotles, and later by Łukasiewicz [Ja´ s69a], the Principle of Non-Contradiction states that two contradictory propositions cannot be simultaneously true. Aristotle considers two kinds of simple propositions, affirmations and denials, which he defines as statements affirming the presence and the absence of a characteristic in a subject, respectively. To Aristotle, the affirmation and denial of a given characteristic in the same subject form a pair of contradictory statements, since from the fact that one is true, it must follow that the other is false, and vice-versa. Then, a logic to reason over Aristotle’s simple propositions must entail a set of rules that ensures it is never possible to derive both an affirmation and its denial as valid conclusions of a given theory, as long as the theory is itself free from contradictions. In bivalent classical logics, the Principle of Non-Contradiction may be formulated in terms of one of the two following rules. Considering a negation connective ¬, which reads as “not”, conjunction ∧, which reads as “and”, and disjunction ∨, which reads as “or”, the first rule, usually referred to as the law of non-contradiction, asserts that a logical contradiction,i.e. a sentence of the form (p∧¬p), is false under all circumstances: that is, a sentence of the form ¬(p∧¬p)is always true, regardless of the meaning of p. This has a direct logical interpretation, it simply says that pand ¬pshould never be simultaneously provable. The other rule, known as the law of the excluded middle, asserts that either p is true or ¬pis true, for any proposition p, implying that a sentence of the form p∨¬pis always provable. It expresses the semantical consideration pointed by Aristotle: if pis true, then ¬pis necessarily false, and vice-versa. Actually, in bivalent classical logic these two rules are derivable from each other, that is, each of them may be defined in terms of the other, and therefore the conclusions one reaches by considering them separately or both together are exactly the same. Nonetheless, it is possible to design other logical systems where these rules are not dual. It is even possible to design logics whose set of rules does not include them, and furthermore it is possible to design logics where some of the connectives we used to state these rules are not even available. . . Aristotle knew, although being convinced that the Principle of Non-contradiction was a fundamental and ultimate truth, that classical logics would not be a universal reasoning tool. For instance, he noticed that modal propositions,i.e. those sentences asserting or denying “possibility or contingency, impossibility or necessity”, would represent an exception to his principle: a sentence like “it may be that. . . ” and its negation are not contradictory statements, but in fact they imply each other. From the fact that “it may be” it follows straightforwardly that “it may not be” as well. He concludes that this kind of propositions have a different behavior with respect to negation than that of simple propositions, but considers that an alternative definition of their contradictory is needed to 3 solve the issue and ensure that the Principle of Non-Contradiction is met. Such sentences are the object of analysis of Modal Logics. Aristotle introduced modal propositions in his Term Logic for syllogisms but “modern” modal logic was founded by C. Lewis, with his famous S-systems [LL34]. A possibility connective 3is used to express the modal status of a proposition p:3preads as “it is possible that p” and ¬3¬p(“it is not possible that not p”) is interpreted as “it is necessary that p”. Because of the duality between possibility and necessity, these are considered ”classical” modal logics. A necessity connective may be introduced in the logic but is redundant, as it can be expressed in terms of 3and ¬. Latter, Kripke developed the possible world semantics for modal logics, based on Leibniz’s conception of possible worlds. The “possible worlds” are understood as points of evaluation, each having its own assignment of truth values for non-modal propositions. A semantic model includes a set of possible worlds and a binary relation, the accessibility relation, establishing “connections” between the worlds, needed for the evaluation of modal propositions. A modal formula 3pis “true” in a world wif pis “true” in at least one world accessible from w;pis “true” if pis “true” in all worlds accessible from w. Łukasiewicz objects that the Principle of Non-Contradiction applies solely to objects from which one obtains a sensible perception and should not be taken as a basic logical principle, “since it is valid only as an assumption”. In fact, a resembling consideration was already pointed out, in different terms, by Aristotle, when explaining why the principle would not apply to modal formulas or sentences of a future tense. That propositions of a future tense represent an objection to the Principle of Non-Contradiction is well illustrated in Aristotle’s famous argument of the sea-fight: in short, there is no way of knowing today which of the sentences “A sea-fight will take place tomorrow” or “A sea-fight will not take place tomorrow” is true, but clearly, either a sea-fight will take place tomorrow or not. Although our intuition that only one of these sentences is true (and the other false) seems correct, which is which is impossible to determine unequivocally. Moreover, this applies to any sentence about a subject whose existence is somehow limited in time, “that which is not always existent or not always nonexistent” - in the Sagirite’s words. Then, the logic that rules what exists actually - at all instants of time - should not be the same as that which rules what exists potentially, also called the undeterminate, since the Principle of Non-Contradiction fails to describe the latter. If, like Aristotle, we accept the undeterminate as an existing object, or moreover, if we acknowledge that existing objects, as in Łukasiewicz formulation, might not be perceptible, then the Principle of Non-Contradiction is no longer a basic logical principle that applies to all existing things. In fairness, even before the Aristotelian principle was formulated, Heraclitus (535 -475 BC) was already convinced that such a principle would fail to describe reality. Instead, based on the assumption that existing objects continuously change throughout time, Heraclitus believed that all things an object can possibly become, including something that is not at a present time, must potentially exist within it at its present 4Chapter 1. Introduction form. An object may have one characteristic today and the opposite characteristic tomorrow and these two contradictory characteristics must potentially exist within it simultaneously. The principle of Non-Contradiction applies to the non-contradictory, but these arguments suggest that some existing things do not conform to the principle because they live in a contradictory state (or do they live in a contradictory state because they do not conform to the principle?). Łukasiewicz also points out the fact that many logical principles hold independently of whether the Principle of Non-Contradiction holds or not and, as mentioned above, there is no reason to believe that a logic allowing contradiction cannot be constructed in the first place. More recently, with the development of quantum theory [BvN37], the mysterious indeterminate object found a concrete physical realization in quantum systems. Indeed, a quantum system may be described by a collection of characteristics, possibly opposite, representing the potential states the system may evolve towards. A paradigmatic example of how a quantum system behaves is that two copies of the same system, meaning that they have exactly the same potentialities, may, upon the same interaction, evolve to different states. Thus, before such interaction, it is not possible to determine, but only to predict, what characteristic will accurately describe the system and, just as the Principle of Non-Contradiction does not apply to the indeterminate object, it does not apply to quantum systems. The notion of consistency is used to characterize logics where no contradictory statements are simultaneously provable, i.e. classical logics. On the other hand, if for a certain logic statements pand ¬pare simultaneously provable, giving rise to what we intuitively call a contradiction, then the logic under consideration is said to be inconsistent. [CCM07] Classical logics become trivial in the presence of contradictions. For example, consider the Propositional Calculus: The statement (p∨¬p)is taken as a rule and thus it is always provable, for any proposition p. Starting with this generic statement and simply applying other rules of the Propositional Calculus, it is possible to derive the rule: (p∧¬p)→q[Com98]. This means that a sentence of the form (p∧¬p)→qis always provable, for any statements pand qin the Calculus. Given a contradictory theory, i.e. a theory which contains at least one contradiction, Propositional Calculus rules of inference set each and every statement in the Calculus as a valid consequence of that theory. In particular, any other contradiction is itself a consequence following from that theory. Ideally, what is fairly inferred from a theory is true: a deductive system which verifies this property is said to be sound. The fact that any statement within the Propositional Calculus, or any other classical logic, is a consequence of a contradictory theory Γis suspicious. Indeed, if a contradiction, which is supposed to be a false statement, is derived from Γ, then classical logics fail to distinguish truth from falsity when reasoning over contradictory theories. That is why under such circumstances, classical logics become trivial: among the 5 conclusions of a contradictory theory are truths and falsities, but the logic fails to make distinction between them. In a sense, truth and falsity collapse into same thing when reasoning over contradictory information. Why reasoning in the presence of contradiction? Logics that become trivial in the presence of a contradiction are said to satisfy the Principle of Explosion or to be explosive. Whenever the Principle of Explosion holds in a logic, a theory where a contradiction occurs entails all possible consequences. In fact, it is the Principle of Explosion that condemns contradictory theories to dud. The sense of studying contradictory theories is recovered as long as they are not trivial. In particular, for an explosive logic, all theories where at least one contradiction occurs are equivalent, since they entail exactly the same set of consequences. It may be difficult to internalize that truth or falsehood may be properly derived from a non-consistent body of knowledge, but it is probably easier to convince ourselves that not all contradictory theories within a logic are equivalent. In order to make distinction between them the Principle of Explosion must be given up. Furthermore, it is quite lazy and unambitious to say that studying nonconsistent bodies of knowledge is worthless, especially with so many real examples where the information at our disposal is even expected to be contradictory. For instance, when we try to track down some event to which there are multiple witnesses it is not surprising that these heterogenous sources may provide conflicting information. The fact that classical logics have their scope of application limited to what is consistent does not challenge their effectiveness in this domain, nor their practical importance. It should be enough evidence to say that classical logic is used to describe the behavior of Boolean circuits which serve as a basis for numerous digital components used nowadays as building blocks of classical computers. That being said, to question the universality of the Principle of Non-contradiction serves the purpose of trying to understand if other domains, besides the consistent one, may be subject to logical reasoning, without detracting from the merits of classical logics. Although Aristotle’s main concern was (probably) to find fundamental truths about the world that surrounds us, logics has throughout the years evolved to a mathematical tool and found lots of practical applications in more specific domains. As said before, there are useful logical systems where the Principle of Non-Contradiction fails and even useful logical systems designed without a negation connective. For instance, the bridge established between logic and computation by the Curry-Howard correspondence equates the natural deduction system (for the positive fragment of the Propositional Calculus) with the λ-calculus and its typing rules. Thus, λ-calculus programs may be reduced to proofs in a deduction system where negation is not available, which is an evidence that the nega- 6Chapter 1. Introduction tion connective is not required for a logic to provide useful reasoning. This may suffice to discard the classical intuition that the Principle of Non-Contradiction should be taken as an axiom of any logic. In removing the connective ¬from Propositional Calculus the theorem (p∨¬p)is also removed, giving a non-explosive version of the Calculus where the statement (p∧¬p)→qis no longer provable. Before we proceed, let us formally define the Principles being evoked. Let Lbe a logic with a set of formulas Fm and a consequence relation , which is monotonic, reflexive and transitive. Let Γ⊆Fm be a theory of L,i.e. a set of formulas closed under the consequence relation. In addition we assume the connective negation ¬is available in L. Principle of Non-Contradiction: Lis non-contradictory if (∃Γ)(∀α∈Fm):Γ1αor Γ1¬α. Principle of Non-Triviality: Lis non-trivial if (∃Γ)(∃α∈Fm):Γ1α. Principle of Explosion: Lis explosive if (∀Γ)(∀α)(∀β)Γ,α,¬αβ. These principles are stated as in [CCM07]. The following assertions are easily seen to be true: a trivial logic is both contradictory and explosive; a contradictory logic is trivial if and only if it is explosive. Contradiction and paraconsistency Reasoning in the presence of contradiction has proved to be particularly useful and important in the discipline of dialectics, where it is accepted that fair conclusions may follow from asserting contradictory propositions. Such a discipline applies, for instance, in resembling debate and trying to establish the truth from conflicting points of view. The Socratic dialogues are a well known form of the dialectic method. Nonetheless, the first system of dialectical logic, where the co-existence of contradictory propositions appears as a fundamental necessity of the reasoning process, is attributed to Hegel [Ja´ s69b], in spite of the large debate on whether Hegel’s dialectical contradictions constitute logical contradictions in the above sense. Assuming this is so, there are still two alternative points of view about Hegel’s dialectics: the first is to consider, like Popper, that (it conforms to classical logic and thus) is trivial; the second is to consider that it does not conform to classical logic, as argued by Priest [PBW18]. Priest is convinced that the central notion of contradiction in Hegel is indeed the logical one and that Hegel’s dialectics is explained by dialetheism,i.e. the view that true logical contradictions, or dialethias, exist, which opposes to the hypothesis sustained by the Principle of Non-Contradiction that all contradictions are necessarily false. In classical logics, the behavior of negation and conjunction (for instance, given in the form of truth tables) is such that a logical contradiction is always a “false” statement. While 7 classical logics have a semantic valuation for propositions which makes them either “true” or “false”, dialetheic logics have a more expressive semantics admitting a third possible truth value that could be read as “true and false”. The introduction of this truth value is justified by the consideration that some propositions are indeed “two-way” truths, where truth and falsity coexist and overlap. In dialetheic logic, the negation of a “true and false” proposition is itself “true and false” and so is the conjunction of two “true and false” propositions. With this artifact it is possible for some contradictions, not all, to be “true and false” which to a dialetheist implies they don’t meet the Aristotelian principle. A logic where the law of non-contradiction does not hold, like dialetheic logic, is said to be paraconsistent. In short, paraconsistent logics exclude the Principle of Explosion, allowing some theories to be contradictory yet non-trivial. Priest suggests that classical logics applies to “the static and changeless”, which are consistent, and that dialetheic logic has a much more general domain, giving a description to what is dynamic as well. The dynamic is by nature contradictory or inconsistent. Indeed, in classical logics, consistency is equated with freedom from contradiction, meaning that once a contradiction occurs, consistency may no longer be recovered. But this notion acquires a more expressive meaning in dialetheic (or more generically, paraconsistent) logics, where it is a characteristic attributable to any proposition. In dialetheic logics, consistent propositions are interpreted as either “true” or “false”, and inconsistent propositions are interpreted as “true and false”. Paraconsistent logics deal with inconsistencies in a more expressive way since contradictions are not necessarily equivalent to one another and not all contradictory theories necessarily entail the same set of consequences. Indirectly, inconsistency has been defined as a glut in a propositions truth value. Paraconsistent logics are then extensions of classical logic, preserving its behavior for what is consistent, represented by truth values “true” and “false”, but endowed with a notion of inconsistency at a propositional level. They are considered weaker forms of classical logics since they extract less consequences from a theory, or at most the same set of consequences. The definition of a Paraconsistent logic as above coincides with Stanislaw Jaskowski formulation [Ja´ s69b]. A logic is paraconsistent if it does not fulfill the Principle of Explosion. This is, for a theory Γof a logic Lin which negation ¬is available (∃Γ)(∃α)(∃β):Γ,α,¬α1β. Another possible definition was pointed out by Newton da Costa who argued that a logic is paraconsistent wrt to negation ¬if it serves as a basis for ¬-contradictory yet non-trivial theories [CCM07] . That is (∃Γ)(∃α)(∃β):(Γαand Γ¬αand Γ1β). Paraconsistent logics are inconsistent, just like trivial logics. But whereas trivial logics allow any inference, the same does not apply to paraconsistent logics. From this fact follows a third definition of a paraconsistent logic: 8Chapter 1. Introduction a logic is paraconsistent if it is inconsistent yet non-trivial. There may be special formulas within a logic, called bottom particles and oftenly denoted by ⊥, which are sufficient to trivialize any theory of a given logic. Formally, a bottom particle ξis such that (∀Γ)(∀β)Γ,ξβ. The symbol ⊥is commonly called absurd or, sometimes, contradiction. In the scope of classical logics, a formula that consists of a contradiction is a bottom particle. In order to dissociate contradiction from triviality it is necessary to establish that a contradiction may or may not be a bottom particle. Paraconsistent logics allow (some) contradictions to be different from the absurd ⊥and that is how contradiction and triviality are turned apart. This could be done, for instance, by defining consistency at a propositional level: then, a consistent proposition is associated with a contradiction which is a bottom particle, whereas an inconsistent proposition is associated with anon-trivial contradiction. Incompleteness and Intuitionism From the definition given above, it is straightforward that the law of non-contradiction fails in a paraconsistent logic but this has no direct implications on its dual, the law of the excluded middle. It is possible to have a paraconsistent logic where the law of the excluded middle holds and, on the other hand, there are logics, termed intuitionistic, where the law of the excluded middle fails but the law of non-contradiction holds. The first system of intuitionistic logic is attributed to Kolmogorov [Usp92], in 1925, but the basic observations leading to the development of this logic are due to Brouwer [vAS15]. Bouwer argues that the law of the excluded middle is abstracted from finite situations and he gives convincing mathematical evidence that it does not extend properly to statements about infinite collections. In classical logics, the law of the excluded middle is sustained by the semantical consideration that truth and falsity are mutually exclusive (they are dual wrt negation and the only available options for assigning a truth value to a proposition). Intuitionistic logic is different because in a sense it allows the truth value of propositions to be left undetermined, thus challenging the law of the excluded middle. As in dialetheic logics, this is achieved by extending semantics to encompass a third truth value, that could read as “neither true nor false”. Classical logic requires knowledge about whether the propositions in a theory are false or true, but in intuitionistic logic the weaker hypothesis that some propositions are not known to be true and not known to be false allows reasoning in a broader domain, starting from much less specific assumptions. These propositions may be defined as vague or as having a gap in their truth value, opposing to those which are distinctly “true” or “false”. While the existence of truth value gluts challenges the law of non-contradiction, the 2 PARACONSISTENT LABELLED TRANSITION SYSTEMS PLTS In a generic Labelled Transition System, connections between states are tagged by some action or program and transitions are regarded as the result of performing such action. In Weighted Transition Systems (WTS) each transition is associated with a numerical value. For example, a particular family of WTS, the Fuzzy Transition Systems, where the weights of transitions belong to the interval [0, 1], is used to capture a notion of uncertainty with respect to the existence of transitions, so that models incorporate transitions for which there is no absolute conviction on whether they are possible or not. Usually in this framework, the weights are not merely numerical values, but elements of a fuzzy truth space, i.e. an algebraic structure over that interval. In this dissertation, we propose a family of transition systems as models to simultaneously characterize information, possibly incomplete or contradictory, regarding the existence and non-existence of a transition between states, in terms of a positive and a negative relation. The first requirement is to define the algebraic structure where the positive and negative relations will take their values and afterwords it is possible to define the model in a generic way. 2.1 truth space Graded transitions considered in the model proposed in this dissertation take values in a truth space whose definition is based on the notion of a residuated lattice [WD38]. Residuated lattices (over a set A) are algebraic structures with signature Σ=hu,t,,,→,eiof arity (2, 2, 2, 2, 0)where: –hA,u,ti is a lattice –hA,,eiis a monoid and – the operation is residuated, with ,→being its right residuum, that is, for all a,b,c∈ A ab≤c⇔b≤a,→c As a direct consequence of this adjunction, we have 16 Chapter 2. Paraconsistent Labelled Transition Systems PLTS if a≤bthen (c,→a)≤(c,→b)(1) if a≤bthen (b,→c)≤(a,→c)(2) We will only consider complete residuated lattices, i.e. lattices where any arbitrary subset of Ahas an infimum and a supremum. Any complete lattice is bounded by a maximal element and a minimal element, which we denote by 1 and 0, respectively. Another requirement is that the residuated lattice is integral, that is, with 1 =e. In an integral residuated lattice the following property, which plays an essential role in the associated logic, holds (see [MNM16] for a proof). a,→(b,→c) = (bua),→c(3) Two other conditions need to be considered. First, a prelinearity condition (a,→b)t(b,→a) = 1 (4) is enforced; the resulting structure is known as a MTL-algebra in the literature [EG01]. The other condition is that ,→is the residuum of u, which leads operations uand to coincide. In this thesis, the term MTL-algebra will be used to refer to a residuated lattice satisfying all the conditions mentioned above. Since the identity of the monoid coincides with the top lattice element and the operations uand coincide, these will be omitted and we will write the tuple A=hA,u,t,1,0,,→i to designate an MTL-algebra. Example 1. 1.1A first example of this structure is a Boolean algebra over {0, 1}, 2=h{0, 1},∧,∨,1,0,→i with the standard interpretation of the Boolean connectives. 1.2Another example, well-known from the fuzzy logic literature, is the G¨ odel algebra G=h[0, 1],min,max, 0, 1, →i where max,min,→:[0, 1]2−→ [0, 1]are defined for any a,b∈[0, 1]as follows. max(a,b) =    aif a≥b botherwise ;min(a,b) =    aif a≤b botherwise ;a→b=   1, if a≤b b, otherwise . 2.1. Truth space 17 The following properties will be needed in the sequel. Lemma 1.Let A=hA,u,t,1,0,,→i be a complete MTL-algebra. Then, for any a1, . . . , an,b∈A b,→l i ai=l i (b,→ai)(5) G i ai,→b=l i (ai,→b)(6) b,→G i ai=G ib,→ai(7) l i ai,→b=G iai,→b(8) where dand Fare the distributed versions of uand t, respectively. The proof of properties Eq. (5) - Eq. (8) can be found in [BEGR09]. Actually, Eq. (5) and Eq. (6) are true for any residuated lattice. One novel aspect of the transition systems we define is that transitions between states are characterized by three distinct components, one being an element of a designated set of atomic actions {p,q,r,s, ...}, interpreted as an action label in Labelled Transition systems, and the other two being elements of an MTL-algebra, which characterize each transition in opposite ways: one represents the evidence of its presence and other the evidence of its absence. We refer to these as the positive accessibility relation and the negative accessibility relation, respectively. Our main concern is to study the case where the positive and negative accessibility relations are elements of an MTL-algebra over [0, 1]. In this fuzzy setting, 0 and 1 are maximal pieces of information; all other values are considered to carry some degree of uncertainty. For each transition, the values of the positive and negative accessibility relations form a pair which may be considered as an element of a bilattice [Gin86], since it is possible to define a truth ordering 4tand an information ordering 4ion such pairs. For a complete lattice hA,≤i, Fitting [Fit89] defines these two orderings as follows: for any (a,b),(c,d) ∈A×A –(a,b)4t(c,d)if and only if a≤cand b≥d –(a,b)4i(c,d)if and only if a≤cand b≤d. As one easily checks, this construction over 2gives Belnap’s bilattice FOUR. Here, the points (a,b),(c,d)such that (a,b)/ 4i(c,d)and (c,d)/ 4i(a,b)are simply (1, 0)and (0, 1), and the points (a0,b0),(c0,d0)such that (a0,b0)/ 4t(c0,d0)and (c0,d0)/ 4t(a0,b0)are simply (1, 1)and (0, 0). Indeed, the definitions given above for the truth and information orderings correctly apply and are in accordance with the interpretation given to the elements in FOUR. However, this construction over a fuzzy lattice has a less convincing interpretation. Consider, as an example, that the pairs (0.1, 0.9)and (0.2, 0.2)are elements of a bilattice h[0, 1]× 18 Chapter 2. Paraconsistent Labelled Transition Systems PLTS [0, 1],4t,4ii. According to the definition, (0.1, 0.9)/ 4i(0.2, 0.2)and (0.2, 0.2)/ 4i(0.1, 0.9). In the present context, the pairs give the evidence of a transition existing and not existing, respectively, so the fact that (0.2, 0.2)/ 4i(0.1, 0.9)misses our intuition that a transition with a positive accessibility relation of 0.1 and a negative accessibility relation of 0.9 is fully characterized, while a transition with positive and negative accessibility relations of 0.2 seem to represent the case where the information about that transition is incomplete. Moreover, one could also ask if there is a more expressive way of ordering the pairs (a,b)and (c,d) such that (a,b)/ 4t(c,d)and (c,d)/ 4t(a,b). Whether it is possible to define a bilattice over truth and information orderings in a more expressive way leaves the scope of this work. Actually, we will consider the pairs defined by the positive and negative accessibility relations as elements of a bilattice A=hA×A,4t ,4iiwhere A=hA,u,t,1,0,,→i is an MTL-algebra and 4t,4iare defined as above. Thus, the information ordering won’t suffice to establish if a particular pair represents a scenario of inconsistency, arising when the values for presence and absence of a transition are contradictory; vagueness, when the values for presence and absence of a transition are neither complementary nor contradictory; or consistency, when the values for presence and absence of a transition are complementary. When Ais a fuzzy lattice, i.e. a lattice over [0, 1], elements of Amay be characterized in terms of their consistency with the help of the conflation operation a, defined for (a,b)∈ A as a(a,b) = (1−b, 1 −a)[Fit89], in the following way: – the pair (a,b)represents inconsistent information, that is, the positive and negative accessibility relations sum to a value greater than or equal to 1, if and only if a (a,b)4i(a,b) – the pair (a,b)represents vague information, or the positive and negative accessibility relations sum to a value less than or equal to 1, if and only if (a,b)4ia(a,b) – the pair (a,b)represents consistent information, or the positive and negative accessibility relations sum to exactly 1, if and only if (a,b)4ia(a,b)and a(a,b)4i(a,b) Pairs containing contradictory information are represented within the upper triangle in Fig. 1, filled in grey. Those for which the information provided is vague lie in the bottom triangle in Fig. 1, filled in pink. And finally consistent pairs are represented by the red line in Fig. 1. The method above applies to bilattices over [0, 1]. However, in Chapter 5we show how to characterize the consistency of elements in a generic bilattice. 2.1. Truth space 19 Transition is present Transition is absent 01 0 1 Figure 1: Intuitionistic (pink), paraconsistent (grey) and classic (red) domains characterizing truth degrees for ”Transition is present” and ”Transition is absent”. Besides conflation, other useful operations may be defined over the bilattice elements characterizing transitions in our model. In particular, some will be important for the definition of the logic in Chapter 4. Definition 1.Given an MTL-algebra A=hA,u,t,1,0,,→i, the algebra A./ =hA,∨ ∨,∧ ∧,=⇒ ,¬i is an A-twist-structure where the twist-operations are defined for (a,b),(a0,b0)∈A×A as follows: –(a,b)∨ ∨(a0,b0) = (ata0,bub0) –(a,b)∧ ∧(a0,b0) = (aua0,btb0) –(a,b) =⇒(a0,b0) = (a,→a0,aub0) –¬(a,b) = (b,a) Originally a ”twist-structure” [Kra98] was defined as a construction over an Heyting algebra, but a construction of this kind had already been proposed under the name of ”special N-lattice” [Vak77] and also over a generic bilattice [Gin88]. In [OW10], for instance, the term twist-structure is used to refer to Ginsberg’s construction over the bilattice FOUR. Although the operation →is the residuum of uin a MTL-algebra, the operation =⇒, which corresponds to the weak implication used in [RJJ15], is not residuated in A./, neither wrt the truth ordering nor wrt the information ordering. If it was, the following conditions would hold: –(a,b)∧ ∧(c,d)4t(e,f)if and only if (c,d)4t(a,b) =⇒(e,f)and –(a,b)∧ ∧(c,d)4i(e,f)if and only if (c,d)4i(a,b) =⇒(e,f). A counter-example using the G¨ odel algebra shows this is not the case. Let (a,b) = (0.8, 0.4), (c,d) = (0.5, 0.2)and (e,f) = (0.6, 0.3). Then (a,b)∧ ∧(c,d) = (min{0.8, 0.5},max{0.4, 0.2}) = (0.5, 0.4)and (a,b) =⇒(e,f) = (0.8 →0.6, min{0.8, 0.3}) = (0.6, 0.3). Indeed, (0.5, 0.4)4t (0.6, 0.3)but (0.5, 0.2)/ 4t(0.6, 0.3). On the other hand, (0.5, 0.2)4i(0.6, 0.3)but (0.5, 0.4)/ 4i(0.6, 0.3). 20 Chapter 2. Paraconsistent Labelled Transition Systems PLTS This result may seem odd, since implication is usually defined as a residuum of conjunction but the idea behind the definition of twist-operations, explained by Vakarelov, is the following. The elements of a twist-structure should be treated as sentences: in this case, each transition is associated with an element (a1,a2)∈A./ where the first component is interpreted as the truth degree of ”transition is present” and the second as the truth degree of ”transition is absent”. Thus a2should be interpreted as a counterexample to a1. For (a1,a2),(b1,b2)∈A./, the twist-operations ∨ ∨,∧ ∧,=⇒and ¬say how to construct classical counterexamples to a1tb1,a1ub1,a1→b1and a2, respectively. The counterexample to a2follows straightforward: it is a1. The counterexamples to a1ub1,a1tb1and ¬a1ub are given by ¬(a1ua2),¬(a1ta2)and ¬(¬a1ub1), which reduce to the expressions in Definition 1with the application of De Morgan’s law. In [Vak77] it is required that the elements (a,b)of a special N-lattice are such that aub= 0wrt to the operation uof the underlying Boolean algebra, which implies that consistency holds for the pairs in a special N-lattice and that there is only one element, i.e. (0, 0), such that (a,b) = ¬(a,b). Although we also interpreter the second element of our twist-structure as a counter-example to the first, we do not impose any consistency requirement, since both values freely take values in the carrier of a residuated lattice, and moreover any element of the form (a,a)satisfies the mentioned property. 2.2 model definition Definition 2.Let A=hA,u,t,1,0,,→i be an MTL-algebra. An A-paraconsistent labelled transition system (A-PLTS) defined over a set of atomic actions Πis a structure hW,Riwhere: -Wis a finite non-empty set whose elements are called worlds or states; -R⊆W×Π×W×A×Ais the (paraconsistent) accessibility relation such that, for any two states w1,w2∈Wand any π∈Π, there is at most one transition (w1,π,w2,α,β)∈R. The relation Rcharacterizes the transitions between states. Each tuple (w1,a,w2,α,β)∈R represents a transition from w1to w2labelled by (a,α,β), where αis the degree to which the action acauses a transition between w1and w2, and βthe degree to which the action a prevents (the occurence of) a transition between w1and w2. Elements in the accessibility relation Rof an A-PLTS are given by tuples, as above, but may be represented in the following manner: w1 (a,α,β) −−−−→ w2≡(w1,a,w2,α,β)∈R . Example 2.Consider the G-PLTS, where Gstands for the G¨ odel algebra, hW,Riover Π= {a,b,c,d}where 2.3. Morphism, Simulation and Bisimulation 21 –W={w1,w2,w3,w4}and –R={(w1,a,w2, 0.7, 0.2),(w2,b,w3, 0.3, 0.5),(w3,c,wc, 0.2, 0.3),(w3,d,w4, 0.5, 0.8)} hW,Riis depicted below. w1 w2w3 w4 (a, 0.7, 0.2)(b, 0.3, 0.5) (c, 0.2, 0.3)(d, 0.5, 0.8) Since the labels in a PLTS quantify the degree to which a transition is present, as well as the degree to which it is absent, it is useful to realize a simple way to access either of these values. We do so by splitting the accessibility relation into a positive accessibility relation and a negative accessibility relation. Thus, for an A-PLTS hW,Riover Πits positive accessibility relation is a function r+: Π−→ AWWsuch that for π∈Πand w,w∈W, r+(π,w,w0) =    αif (w,π,w0,α,β)∈R 0 otherwise Similarly, its negative accessibility relation is a function r−:Π−→ AWWsuch that for π∈Πand w,w∈W, r−(π,w,w0) =    βif (w,π,w0,α,β)∈R 1 otherwise We also use the terms ”positive accessibility relation” and ”negative accessibility relation” to refer to the values yield by the functions r+and r−for each particular transition of a PLTS. In general, these values will be elements of an MTL-algebra and form a pair which is an element of a bilattice and also of a twist-structure over that bilattice. 2.3 morphism,simulation and bisimulation Definition 3.Let A=hA,u,t,1,0,,→i be an MTL-algebra and let T1=hW1,R1i,T2= hW2,R2ibe two A-PLTS defined over the same set of actions Π. Denote the positive and negative accessibility relations for T1and T2by r+ 1,r− 1and r+ 2,r− 2, respectively. A morphism 22 Chapter 2. Paraconsistent Labelled Transition Systems PLTS relating these two PLTS is a function h:W1→W2such that ∀π∈Π,r+ 1(π,w1,w2)≤ r+ 2(π,h(w1),h(w2)) and r− 1(π,w1,w2)≥r− 2(π,h(w1),h(w2)). Example 3.For Π={a,b,c,d}consider two G-PLTS M1and M2given by the following diagrams. w1 w2w3 w4 (a, 0.7, 0.2)(b, 0.3, 0.5) (c, 0.2, 0.3)(d, 0.5, 0.8) v1 v2v3 v4 v5 (a, 0.9, 0.1)(b, 0.5, 0.2) (c, 0.6, 0.1)(c, 0.8, 0.4) (a, 0.4, 0.7) The mapping h={w17→ v1,w27→ v2,w37→ v3}is a morphism. It is easy to check that h satisfies the conditions of Definition 3. Definition 4.Let A=hA,u,t,1,0,,→i be an MTL-algebra and let T1=hW1,R1i,T2= hW2,R2ibe two A-PLTS defined over the same set of actions Π. Denote the positive and negative accessibility relation functions for T1and T2by r+ 1,r− 1and r+ 2,r− 2, respectively. A relation S⊆W1×W2is a simulation provided that, for all hp,qi ∈ S, the following condition holds: - if there is a transition in T1from pto p0caused by a∈Π, then there is a transition in T2from qto q0caused by asuch that r+ 2(a,q,q0)≥r+ 1(a,p,p0),r− 2(a,q,q0)≤r− 1(a,p,p0)and hp0,q0i ∈ S. In short, S⊆W1×W2is a simulation if, for all hp,qi ∈ Sand a∈Π, p(a,α,β) −−−−→T1p0⇒ h∃q0∈W2,∃γ,δ∈[0, 1]:q(a,γ,δ) −−−−→T2q0∧hp0,q0i ∈ S∧γ≥α∧δ≤βi. From here on, the following abbreviation is used to represent the above condition: p(a,α,β) −−−−→T1p0⇒ h∃q0∈W2:q(a,γ:γ≥α,δ:δ≤β) −−−−−−−−−−−→T2q0∧hp0,q0i ∈ Si. Two states pand qare similar, written p.q, if there is a simulation Ssuch that hp,qi ∈ S. Example 4.In the G-PLTS given by the diagrams below, w1.v1, because there is a simulation, S={hw1,v1i,hw2,v2i,hw3,v2i,hw4,v3i,hw5,v4i}, that contains hw1,v1i. 2.3. Morphism, Simulation and Bisimulation 23 w1w2 w3 w4 w5 (a, 0.4, 0.7) (a, 0.3, 0.6) (b, 0.2, 0.8) (c, 0.2, 0.9) v1v2v3 v4 (a, 0.5, 0.5) (b, 0.3, 0.5) (c, 0.5, 0.5) Lemma 2.The similarity relation is a preorder, i.e. a reflexive and transitive relation. Proof. (i) Reflexivity: p.p This follows from the fact that the identity relation is a simulation. Indeed, for a PLTS hW,Ri, the relation S⊆W×Wsuch that hw,wi ∈ Sfor all w∈Wsatisfies the conditions of Definition 4. (ii) Transitivity: if p.S1qand q.S2tthen p.S3t p.S1q⇒ ∃ a simulation S1:hp,qi ∈ S1 q.S2t⇒ ∃ a simulation S2:hq,ti ∈ S2 To prove that p.twe must find a simulation S3such that hp,ti ∈ S3. Let S3=S2·S1. Indeed, hp,ti ∈ S3since hp,qi ∈ S1and hq,ti ∈ S2. Now we must prove S3satisfies the conditions in Definition 4. hp,qi ∈ S1⇒if p(a,α,β) −−−−→T1p0then h∃q0:q(a,γ:γ≥α,δ:δ≤β) −−−−−−−−−−−→T2q0∧hp0,q0i ∈ S1i But since hq,ti ∈ S2then ∃t0:t(a,µ:µ≥γ,ν:ν≤δ) −−−−−−−−−−−→T3t0∧hq0,t0i ∈ S2i It is straightforward that µ≥γ⇒µ≥αand ν≤δ⇒ν≤β. Thus, for hp,ti ∈ S3, p(a,α,β) −−−−→T1p0⇒ h∃t0:t(a,µ:µ≥α,ν:ν≤β) −−−−−−−−−−−→T3t0i. To check that hp0,t0i ∈ S3just notice that hp0,q0i ∈ S1and hq0,t0i ∈ S2. Definition 5.Two states pand qare equisimilar if q.S1qand q.S2p. Example 5.Consider the two G-PLTS depicted below and a relation S={hw1,v1ihw2,v2i,hw3,v2i}. We have w1.Sv1and v1.Sw1, so w1and v1are equisimilar. 24 Chapter 2. Paraconsistent Labelled Transition Systems PLTS w1 w2w3 (a, 0.5, 0.3) (a, 0.7, 0.2) (c, 0.2, 0.3) (c, 0.4, 0.5) (c, 0.4, 0.5) v1 v2 (a, 0.7, 0.2) (c, 0.4, 0.5) Definition 6.Let A=hA,u,t,1,0,,→i be an MTL-algebra and let T1=hW1,R1iand T2= hW2,R2ibe two A-PLTS defined over the same set of actions Π. A relation B⊆W1×W2is abisimulation if for hp,qi ∈ Band a∈Π p(a,α,β) −−−−→T1p0⇒ h∃q0∈W2:q(a,α,β) −−−−→T2q0∧hp0,q0i ∈ Biand q(a,α,β) −−−−→T2q0⇒ h∃p0∈W1:p(a,α,β) −−−−→T1p0∧hp0,q0i ∈ Bi. It follows straightforward that any transition in the first PLTS is mapped to an exactly equal transition in the second PLTS, and vice-versa. Thus, the bisimulation is an equivalence relation, i.e. a reflexive, transitive and symmetric relation. Two states pand qare bisimilar, written p∼q, if there is a bisimulation Bsuch that hp,qi ∈ B. 2.4 traces and trace equivalence Let A=hA,u,t,1,0,,→i be an MTL-algebra and hW,Ribe an A-PLTS defined over a set of actions Π. Furthermore let r+,r−denote its positive and negative accessibility relations, respectively. Definition 7.Apath from w∈Win a PLTS hW,Riis a sequence [(w1,a1,w2),(w2,a2,w3), ...] such that wi∈W,ai∈Πof worlds connected by transitions available in hW,Ri, with w1=w. The set of all paths from wis denoted by Paths(w). Example 6.Consider the PLTS given in Example 2. The following are some paths from w1: [(w1,a,w2)],[(w1,a,w2),(w2,b,w3)],[(w1,a,w2),(w2,b,w3),(w3,c,w2)]. Note that a path, as defined above, only specifies the action causing each transition, and leaves out the values for the accessibility relations. These values are easily obtained using r+ and r−: for each tuple (w,a,w0)in a path, r+(a,w,w0)and r−(a,w,w0)are the values for the accessibility relation characterizing the transition to which the tuple refers. We define the function t:W×Π×W→Π×A×Asuch that t(w,a,w0) = (a,r+(a,w,w0),r−(a,w,w0)). Thus, from a path ρ= [(w1,a1,w2),(w2,a2,w3), ...]one obtains a sequence of transition labels in a PLTS by mapping each (wi,aj,wk)in ρto t(wi,aj,wk). The list trait(ρ) = t∗(ρ)is the list derived by successively applying tto the tuples in ρand we call it trait of ρ. 3.1. Restriction 31 1. there is a unique morphism ! : T→Tnil, given by ((!W,()), where !W(i) = ∗and (w,a,w0,α,β)∈R⇒(∗,⊥,∗, 1, 0)∈RTnil ⊥. 2. Similarly, there is a unique morphism ? : Tnil →T, given by (i,()). Clearly, i(∗) = i and the other condition is necessarily true. Given a PLTS T=hW,i,R,Πi, a world w∈Wis reachable if there is a path in T from ito w. We follow the terminology in [WN95] and say Tis reachable if it is possible to reach every world of Tstarting from the initial state. Furthermore, Tis acyclic if there is only one path from each world to itself and it is an idle transition. Morphisms preserve the initial state and also reachable states: that is, if wis reachable in Tand there is a morphism (σ,λ):T→T0, then σ(w)is reachable in T0. 3.1 restriction In a generic labelled transition system, the operation of restriction takes a subset of the system’s set of labels and removes all transitions whose labels are not in that set. Since the labels represent actions causing transitions, the operation of restriction narrows the actions that the system is able to perform. PLTS have labels with three distinct components but only one refers to the actions causing transitions, thus the operation of restriction has its version on the PLTS setting. Definition 12.Let T=hW,i,R,Πibe a PLTS. For Π0⊂Πlet λ:Π0→Πbe a mapping taking a∈Π0to a∈Π. The restriction Tλis a PLTS hW,i,R0,Π0iover Π0where R0={(w,π,w0,α,β)∈R|π∈Π0}. There is an extended morphism from the restricted PLTS Tλto the original one, given by f= (1W,λ)and a functor p:TPL →Set∗between the category TPL and the category of sets with partial functions, which sends a morphism (σ,λ):T1→T2of PLTS T1=hW1,i1,R1,Π1iand T2=hW2,i2,R2,Π2i, to the partial function λ:Π1→Π2. The morphism fassociated with the restriction is a cartesian morphism in TPL, since it satisfies the following universal property: For any morphism g :T0→T in TPL such that p(g) = λthere is a unique morphism h:T0→TL such that p(h) = 1Π0and f ◦h=g. In a diagram: 32 Chapter 3. Constructions over PLTS T0 TλT hg f Π0Π λ A cartesian morphism f= (σ,λ)in TPL is a cartesian lifting of the morphism p(f) = λ in Set∗. In general, the operation of restriction does not preserve the reachable states. Example 11.Consider the PLTS Tdepicted below, with initial state i. iw2w3w4 (a, 1, 0) (b, 1, 0) (c, 1, 0) The restriction T{a,c}is the PLTS: iw2w3w4 (a, 1, 0) (c, 1, 0) Which clearly has a distinct set of reachable states from i. Now consider the following PLTS T0. i0w0 2 (a, 1, 0) The state iof T{a,c}from Example 11 is bisimilar to the state i0of T0. In terms of reachable states, T0and T{a,c}have the same behaviors. Thus it could be useful to have an additional construction giving the reachable component of a (restricted) PLTS. Definition 13.Let T=hW,i,R,Πibe a PLTS. The reachable component of T is the PLTS Treach =hW0,i,R0,Π0iwhere R0={(w,a,w0,α,β)∈R|w=i}∪{(w,a,w0,α,β)∈R|there is a path in T from ito w}. W0is the set of reachable worlds in Tand Π0is the set of actions labelling the transitions in Treach. Clearly, W0⊆Wand Π0⊆Π. 3.2. Relabelling 33 3.2 relabelling Given a labelled transition system Twhose labelling set is Πand a total function λ:Π→ Π0, the relabelling construction preserves the underlying structure of Tbut consistently changes its labels according to λ. In essence, this construction renames the actions in T. It is also possible to define a construction which renames the actions in a PLTS. Definition 14.Let T=hW,i,R,Πibe a PLTS. Let λ:Π→Π0be a total function. The relabelling T{λ}is the PLTS hW,i,R0,Π0iwhere R0={(w,λ(a),w0,α,β)|(w,a,w0,α,β)∈R} There is a morphism from a PLTS Tto the relabeled PLTS T{λ}, given by f= (1W,λ) and it is a cocarteasian morphism, since it satisfies the following universal property: For any morphism g :T→T0in TPL such that p(g) = λ, there is a unique morphism h:T{λ} → T0such that p(h) = 1Π0and h ◦f=g. In a diagram: T0 T{λ} Tf gh ΠΠ0 λ A cocartesian morphism in TPL is associated with a construction dual to the cartesian lifting, which is the cocartesian lifting. Then, a cocartesian morphism f= (σ,λ)in TPL is a cocartesian lifting of the morphism p(f) = λin Set∗. 3.3 parallel composition The product of two transition systems is an operation for producing a parallel composition of the two systems. The parallel composition of two systems models a process combining the execution of all processes inherent to each component system. Essentially, states of the product system are obtained through the combination of a state from each component system, and, similarly, transitions are obtained through the combinations of a transition from each component system (idle transitions included). In [WN95] parallelism is modeled through the construction of a product, which combines the two systems allowing all conceivable synchronizations. That is, any combination of states of the component systems is 34 Chapter 3. Constructions over PLTS a valid state in the product system and any transition in the first component system may be performed synchronously with any other transition from the second component system. For this reason, the product operation is combined with the operations of restriction and relabelling in order to remove unwanted synchronizations and produce more specific parallel compositions. The product of two generic LTS is a LTS where transitions are either caused by performing one action in each component system at the same time, or by performing an action at a time in one of the component systems. Definition 15.Let T1=hW1,i1,R1,Π1iand T2=hW2,i2,R2,Π2ibe two PLTS. Their product T1×T2is the PLTS hW1×W2,(i1,i2),R,Πi, such that –Π=Π1×⊥Π2={(a,⊥)|a∈Π1}∪{(⊥,b)|b∈Π2}∪{(a,b)|a∈Π1,b∈Π2}, and –(w,a,w0,α,β)∈Rif and only if (P1(w),P1(a),P1(w0),α1,β1)∈R⊥ 1and (P2(w),P2(a),P2(w0),α2,β2)∈R2∗and α=α1uα2and β=β1tβ2. The set of actions of a product has elements of the form (a,b), which represent synchronizations between the component processes, that is, the execution of an action by each component simultaneously; and elements of the form (a,⊥)or (⊥,b), which represent the execution of an action by one of the component systems and inaction in the other. The product T1×T2=hW,i,R,Πiof two PLTS has projection morphisms P:T1×T2→⊥ T1and P0:T1×T2→⊥T2given by P= (P1,P1)and P0= (P2,P2). For a synchronous transition (w,e,w0,α,β)it follows straightforward from Definition 15 that there is a transition (P1(w),P1(e),P1(w0),α1,β1)∈R1such that α≤α1and β≥β1; and a transition (P2(w),P2(e),P2(w0),α2,β2)∈R2such that α≤α2and β≥β2. For asynchronous transitions (w,(⊥,b),w0,α,β)or (v,(a,⊥),v0,α0,β0), note that P1(w) = P1(w0)and P2(v) = P2(v0) and indeed (P1(w),⊥,P1(w0), 1, 0)∈R⊥ 1and (P2(v),⊥,P2(v0), 1, 0)∈R⊥ 2. For any values of α,α0,β,β0it is true that α≤1, α0≤1, β≥0 and β0≥0. These two morphisms form a product in TPL since they satisfy the following universal property: For any morphism g1:T→T1and g2:T→T2, there is a unique morphism h :T→T1×T2, given by hg1,g2i, such that P◦h=g1and P0◦h=g2. In a diagram: T1T1×T2T2 T P P0 h g1g2 Proof. To check that the diagram commutes just note that: 3.3. Parallel composition 35 –(P◦h)(x) = P(hg1(x),g2(x)i) = g1(x)and –(P0◦h)(x) = P0(hg1(x),g2(x)i) = g2(x). We must also prove that his a morphism and that it is unique. Let T=hW,i,R,Πi,T1= hW1,i1,R1,Π1i,T2=hW2,i2,R2,Π2i,T1×T2=hW1×W2,(i1,i2),R0,Π0i,g1= (σ1,λ1)and g2= (σ2,λ2). If (w,a,w0,α,β)∈Rthen there is a transition (σ1(w),λ1(a),σ1(w0),α1,β1)∈ R⊥ 1such that α≤α1and β≥β1; and also a transition (σ2(w),λ2(a),σ2(w0),α2,β2)∈R⊥ 2 such that α≤α2and β≥β2. Moreover, according to 15 there is a transition (hσ1,σ2i(w),hλ1,λ2i(a),hσ1,σ2i(w0),α1uα2,β1tβ2)∈R0 . Thus for any (w,a,w0,α,β)∈Rthere is a transition (hσ1,σ2i(w),hλ1,λ2i(a),hσ1,σ2i(w0),α0,β0)) ∈R0 such that α≤α0and β≥β0. Furthermore, initial states are preserved since hσ1,σ2i(i) = (σ1(i),σ2(i)) = (i1,i2)so h=hg1,g2iis a morphism. Let f:T→T1×T2be some other morphism such that P◦f=g1and P0◦f=g2. For some xlet f(x) = ha,bi. Then we have g1(x)=(P◦f)(x) = P(f(x)) = Pha,bi=aand g2(x) = (P0◦f)(x) = P0(f(x)) = P0ha,bi=b. Therefore f(x) = hg1(x),g2(x)i=h(x), which proves f=hand thus there is a unique morphism satisfying the universal property. A state sis reachable in T1×T2if and only if P1(s)is reachable in T1and P2(s)is reachable in T2. We have only considered binary products but all products exist in TPL, in particular the empty product which is Tnil. Example 12.Consider the PLTS T1and T2depicted below. i1w (a, 0.7, 0.2) i2v (b, 0.4, 0.6) Their product Tis the PLTS 36 Chapter 3. Constructions over PLTS (i1,i2) (w,i2) (w,v)(i1,v) ((a,⊥), 0.7, 0.2) ((⊥,b), 0.4, 0.6) ((a,b), 0.4, 0.6) ((⊥,b), 0.4, 0.6) ((a,⊥), 0.7, 0.2) As mentioned above, it is possible to remove unwanted transitions in a PLTS that consists in the product of two transition systems by simply applying operation(s) of restriction. For instance, the parallel composition of two systems where no transitions may be performed simultaneously could be obtained through the construction of the product and then restriction to all possible synchronizations. Definition 16.Let T1=hW1,i1,R1,Π1i,T2=hW2,i2,R2,Π2ibe two PLTS and T1×T2= hW0,i0,R0,Π1×⊥Π2ibe their product. Also let Π={(a,⊥)|a∈Π1}∪{(⊥,b)|b∈Π2}and λ:Π→Π1×⊥Π2be the mapping taking x∈Πto x∈Π1×⊥Π2. The interleaving or asynchronous product T1|||T2≡(T1×T2)λis the PLTS hW1×W2,(i1,i2),R,Πisuch that R={(w,a,w0,α,β)∈R0|a∈Π}. Example 13.For the PLTS in Example 12 this gives the PLTS depicted below. (i1,i2) (w,i2) (w,v)(i1,v) ((a,⊥), 0.7, 0.2) ((⊥,b), 0.4, 0.6)((⊥,b), 0.4, 0.6) ((a,⊥), 0.7, 0.2) On the other hand, the parallel composition of two systems where only synchronous transitions are allowed could be obtained through the construction of the product and then restriction to all asynchronous transitions. Definition 17.Let T1=hW1,i1,R1,Π1i,T2=hW2,i2,R2,Π2ibe two PLTS and T1×T2= hW0,i0,R0,Π1×⊥Π2ibe their product. Also let Π={(a,b)|a∈Π1and b∈Π2}and 3.4. Sum 37 λ:Π→Π1×⊥Π2be the mapping taking x∈Πto x∈Π1×⊥Π2. The synchronous product T1⊗T2≡(T1×T2)λis the PLTS hW1×W2,(i1,i2),R,Πisuch that R={(w,a,w0,α,β)∈R0|a∈Π}. Example 14.For the PLTS in Example 12 this gives the PLTS depicted below. (i1,i2) (w,i2) (w,v)(i1,v) ((a,b), 0.4, 0.6) 3.4 sum In process calculi the (nondeterministic) sum of two or more processes defines a process that can behave as each of its component processes. The sum of transition systems must be a construction capturing this property so it is capable of simulating the behavior of the alternative processes modeled by its constituent systems. Definition 18.Let T1=hW1,i1,R1,Π1iand T2=hW2,i2,R2,Π2ibe two PLTS. Their sum T1+T2is the PLTS hW,(i1,i2),R,Π1∪Π2i, where –W= (W1×{i2})∪({i1}×W2), –t∈Rif and only if ∃(w,a,w0,α,β)∈R1such that t= (In1(w),a,In1(w0),α,β)or ∃(w,a,w0,α,β)∈R2such that t= (In2(w),a,In2(w0),α,β) where In1and In2are the left and right injections, respectively. Associated with the sum T1+T2there are injection morphisms I1:T1→T1+T2and I2:T2→T1+T2given by I1= (In1, 1Π)and I2= (In2, 1Π). These two morphisms form a coproduct in TPL, since they satisfy the following universal property: For any morphisms g1:T1→T and g2:T2→T, there is a unique morphism h :T1+T2→T, given by [g1,g2], such that h ◦I1=g1and h ◦I2=g2. In a diagram: T1T1+T2T2 T I1I2 h g1g2 38 Chapter 3. Constructions over PLTS Proof. To check that the diagram commutes just note that: –(h◦I1)(x) = [g1,g2](I1(x)) = g1(x) –(h◦I2)(x) = [g1,g2](I2(x)) = g2(x) We must also prove that his a morphism and that it is unique. Let T=hW,i,R,Πi, T1=hW1,i1,R1,Π1i,T2=hW2,i2,R2,Π2i,T1+T2=hW0,(i1,i2),R0,Π0i,g1= (σ1,λ1)and g2= (σ2,λ2). If (w,a,w0,α,β)∈R1then there is a transition (σ1(w),λ1(a),σ1(w0),α1,β1)∈ Rsuch that α≤α1and β≥β1; and also a transition (In1(w),a,In1(w0),α,β)∈R0. If (w,a,w0,α,β)∈R2then there is a transition (σ2(w),a,σ2(w0),α2,β2)∈Rsuch that α≤α2and β≥β2; and also a transition (In2(w),a,In2(w0),α,β)∈R0. Thus for any (w,a,w0,α,β)∈R0there is a transition ([σ1,σ2](w),[λ1,λ2](a),[σ1,σ2](w0),α0,β0)∈Rsuch that α≤α0and β≥β0. Furthermore, initial states are preserved since σ1(i1) = σ2(i2) = i, so h= [g1,g2]is a morphism. Now let f:T1+T2→Tbe some other morphism such that f◦I1=g1and f◦I2=g2. Then g1(x) = (f◦I1)(x) = f(I1(x)) and g2(x) = ( f◦I2)(x) = f(I2(x)). On the one hand we have [g1,g2](x) = [f(I2(x)),f(I2(x))], and on the other hand [g1,g2](x) = [g1(x),g2(x)] = [h(I1(x)),h(I2(x))]. Thus f=hand there is a unique morphism satisfying the universal property. A state sis reachable in T1+T2if there is s1reachable in T1such that s=In1(s1)or there is s2reachable in T2such that s=In2(s2). We have only considered the coproduct of two PLTS, but all coproducts exist in TPL. Example 15.Consider the PLTS T1and T2depicted below. i1w (a, 0.7, 0.2) i2v (b, 0.4, 0.6) Their sum Tis the PLTS (i1,i2) (w,i2) (i1,v) (a, 0.7, 0.2) (b, 0.4, 0.6) 3.5. Prefixing 39 3.5 prefixing The operation of prefixing in a generic LTS adds a new initial state and introduces a transition connecting it to the former initial state. The process resulting from this operations behaves as the original process after the new initial action has taken place. Then, from a given LTS one constructs a prefix of it by specifying the label for the new transition. We add a new transition to construct the prefix of a PLTS by specifying not only the action causing the transition but also the values for the positive and negative accessible relation. Definition 19.Let T=hW,i,R,Πibe a PLTS over an MTL-algebra A=hA,u,t,1,0,,→i . Given an action {a}, eventually not in Π, and α,β∈Athe prefix (a,α,β)Tis a construction that gives the PLTS T0=hW0,i0,R0,Π∪{a}i where –W0={w|w∈W}∪{∅}, –i0=∅ –R0={(w,π,w0,α0,β0)|(w,π,w0,α0,β0)∈R}∪{(∅,a,i,α,β)} Since it is not required that the prefixing action is distinct from the former actions, the operation of prefixing does not extend to a functor in TPL. This is illustrated in the example below. Example 16.Consider two PLTS T1=hW1,i1,R1,Π1iand T2=hW2,i2,R2,Π2idepicted below. i1w (a, 0.7, 0.2) i2v (b, 0.8, 0.1) There is an extended morphism (σ,λ):T1→T2given by σ(i1) = i2,σ(w) = vand λ(a) = b. 16.1Now consider the prefixes (a, 1, 0)T1and (a, 1, 0)T2depicted below. ii1w (a, 1, 0) (a, 0.7, 0.2) i0i2v (a, 1, 0) (b, 0.8, 0.1) Clearly, a mapping from the actions in (a, 1, 0)T1to the actions in (a, 1, 0)T1does not exist so neither exists a morphism between the two prefixes. 16.2If we consider prefixes where the transition from the initial state is caused from a fresh action, i.e. some action csuch that c/∈Π1tΠ2, such as the prefixes (c, 1, 0)T1 and (c, 1, 0)T2, depicted below, there is an extended morphism (σ0,λ0):(c, 1, 0)T1→ (c, 1, 0)T2given by 40 Chapter 3. Constructions over PLTS –σ0(x) =    σ(x)if x∈W1tW2 i0if x=i –λ0(x) =    λ(x)if x∈Π1tΠ2 x0otherwise ii1w (c, 1, 0) (a, 0.7, 0.2) i0i2v (c, 1, 0) (b, 0.8, 0.1) However, the operation of prefixing extends to a functor on the subcategory of actionpreserving morphisms, i.e. the subcategory where morphisms (σ,λ)between PLTS are such that λis an inclusion function. Given two PLTS T1=hW1,i1,R1,Π1i,T2=hW2,i2,R2,Π2 and an action-preserving morphism (σ,λ):T1→T2there is a functor which sends (σ,λ) to a morphism (σ0,λ0):(a,α,β)T1→(a,α,β)T2, for some action aand some α,β∈A, given by: –σ0(x) =    ø if x=ø σ(x)otherwise –λ0(x) = x 3.6 other operations There are of course several constructions one may perform to obtain a modified transition system from a given one (or more). Those constructions are defined depending on what is useful for different kinds of transition systems and their applications. One particularity of PLTS is that of having transitions with two accessibility relations, besides the typical labelling action, and for that reason we propose some operations which have no analogous in [WN95], but are designed specifically for PLTS over the G¨ odel algebra G. First we define an operation which takes a PLTS and uniformly increases or decreases the value of the positive accessibility relation in all transitions and another one which uniformly increases or decreases the value of the negative accessibility relation. For this purpose we define the following operation for α,β∈[0, 1] α⊕β=         1 if α+β≥1 0 if α+β≤0 α+βotherwise Definition 20.Let T=hW,i,R,Πibe a PLTS. Taking v∈[−1, 1], the positive v-approximation T⊕+ vis a PLTS hW,i,R0,Πiwhere 4.2. Semantics and Satisfaction 47 1. Then, in order to prove (1), we observe that (w|=> ↔ ∼⊥) ={(12)} ((w|=>) =⇒(w|=∼⊥))∧ ∧((w|=∼⊥) =⇒(w|=>)) ={definition of |=} ((1, 0) =⇒(w|=⊥ → ⊥))∧ ∧((w|=⊥ → ⊥) =⇒(1, 0)) ={definition of |=} ((1, 0) =⇒((0, 1) =⇒(0, 1))) ∧ ∧(((1, 0) =⇒(0, 1))) =⇒(1, 0)) ={definition of =⇒} ((0, 1) =⇒(1, 0))∧ ∧((1, 0) =⇒(1, 0)) ={definition of =⇒} (1, 0)∧ ∧(1, 0) ={definition of ∧ ∧} (1, 0) 2. In order prove (2) let us consider fix (w|=ϕ1) = (α,β)and (w|=ϕ2) = (α0,β0). 48 Chapter 4. MIPL - A modal intuitionistic paraconsistent logic (w|=∼(ϕ1∧ϕ2)) ={definition of ∼} w|= (ϕ1∧ϕ2)→ ⊥ ={definition of |=} (w|= (ϕ1∧ϕ2))=⇒(w|=⊥) ={definition of |=} ((w|=ϕ1)∧ ∧(w|=ϕ2))=⇒(0, 1) ={(12)} (α,β)∧ ∧(α0,β0)=⇒(0, 1) ={definition of ∧ ∧} (αuα0,βtβ0) =⇒(0, 1) ={definition of =⇒} ((αuα0),→0, αuα0) (w|= (∼ϕ1∨∼ϕ2)) ={definition of |=} (w|=∼ϕ1)∨ ∨(w|=∼ϕ2) ={definition of ∼} ((w|=ϕ1) =⇒(0, 1))∨ ∨ ((w|=ϕ2) =⇒(0, 1)) ={−} ((α,β) =⇒(0, 1))∨ ∨ (α0,β0) =⇒(0, 1) ={definition of =⇒} (α,→0, α)∨ ∨(α0,→0, α0) ={definition of ∨ ∨} (α→0tα0→0, αuα0) By Eq. (8) in Lemma 1,((αuα0),→0, αuα0) = (α,→0tα0,→0, αuα0). Hence w|=∼(ϕ1∧ϕ2)↔(∼ϕ1∨∼ϕ2). 3. In order to prove (3) let us consider fix (w|=ϕ1) = (α,β)and (w|=ϕ2) = (α0,β0). 4.2. Semantics and Satisfaction 49 (w|=∼(ϕ1∨ϕ2)) ={definition of ∼} w|= (ϕ1∨ϕ2)→ ⊥ ={definition of |=} (w|= (ϕ1∨ϕ2))=⇒(w|=⊥) ={definition of |=} ((w|=ϕ1)∨ ∨(w|=ϕ2))=⇒(0, 1) ={(12)} (α,β)∨ ∨(α0,β0)=⇒(0, 1) ={definition of ∨ ∨} (αtα0,βuβ0) =⇒(0, 1) ={definition of =⇒} ((αtα0),→0, αtα0) (w|= (∼ϕ1∧∼ϕ2)) ={definition of |=} (w|=∼ϕ1)∧ ∧(w|=∼ϕ2) ={definition of ∼} ((w|=ϕ1) =⇒(0, 1))∧ ∧ ((w|=ϕ2) =⇒(0, 1)) ={−} ((α,β) =⇒(0, 1))∧ ∧ (α0,β0) =⇒(0, 1) ={definition of =⇒} (α,→0, α)∧ ∧(α0,→0, α0) ={definition of ∧ ∧} (α,→0uα0,→0, αtα0) By Eq. (6) in Lemma 1,((αtα0),→0, αtα0) = ((α,→0)u(α0,→0),αtα0). Hence (w|=∼(ϕ1∨ϕ2)) = (w|= (∼ϕ1∧∼ϕ2)). Remark 2.Note that the definition ∼coincides with the definition of classic and intuitionistic logic. Intristingly, De Morgan duality applies to ∧and ∨wrt ∼, which is not the case in intuitionistic logic. On the other hand, the rules of material implication and double negation are not valid for ∼ and the rule of material implication is not valid for ¬. This means that ∼and ¬do not satisfy the axioms of an intuitionistic negation and moreover they do not satisfy the axioms of a strong negation. (For the definition of strong negation see for instance [Sed16] or [Vak77].) Indeed, ¬ϕ→ ∼ϕand ∼ϕ→ ¬ϕare not valid formulas in MIPL so neither of these negations is ”stronger” than the other. It is clear from Definition 24 that modal operators are not dual in the classical sense. Nonetheless we shall prove the following equalities between modal formulas. Theorem 2.The following semantical equivalences are true in any MIPL model: ¬ϕ≡ ¬3ϕ(13) 3¬ϕ≡ ¬ ϕ(14) /¬ϕ≡/ 3ϕ(15) / 3¬ϕ≡/ϕ(16) ∼ϕ≡ ∼3ϕ(17) /∼ϕ≡ ¬∼/ 3ϕ(18) 50 Chapter 4. MIPL - A modal intuitionistic paraconsistent logic Proof. (i) (¬ϕ) = ¬(3ϕ) (w|=¬ϕ) ={definiton of |=} l w0∈W{R+(w,w0),→(w0|=¬ϕ)+},G w0∈W{R+(w,w0)u(w0|=¬ϕ)−}! ={definition of |=} l w0∈W{R+(w,w0),→(¬(w0|=ϕ))+},G w0∈W{R+(w,w0)u(¬(w0|=¬ϕ))−}! ={definition of ¬} l w0∈W{R+(w,w0),→(w0|=ϕ)−},G w0∈W{R+(w,w0)u(w0|=ϕ)+}! ={definition of ,3 + } ((w,ϕ,−),3 + (w,ϕ,+)) ={definition of ¬} ¬(3 + (w,ϕ,+),(w,ϕ,−)) ={definition of |=} (w|=¬(3ϕ)) (ii) 3(¬ϕ) = ¬(ϕ) 4.2. Semantics and Satisfaction 51 (w|=3(¬ϕ)) ={definition of |=} G w0∈W{R+(w,w0)u(w0|=¬ϕ)+},l w0∈W{R+(w,w0),→(w0|=¬ϕ)−}! ={definition of |=} G w0∈W{R+(w,w0)u(¬(w0|=ϕ))+},l w0∈W{R+(w,w0),→(¬(w0|=ϕ))−}! ={definition of ¬} G w0∈W{R+(w,w0)u(w0|=ϕ)−},l w0∈W{R+(w,w0),→(w0|=ϕ)+}! ={definition of 3 + ,} (3 + (w,ϕ,−),(w,ϕ,+)) ={definition of ¬} ¬((w,ϕ,+),3 + (w,ϕ,−)) ={definition of |=} (w|=¬(ϕ)) (iii) /¬ϕ=/ 3ϕ 52 Chapter 4. MIPL - A modal intuitionistic paraconsistent logic (w|=/(¬ϕ)) ={definition of |=} G w0∈W{R−(w,w0)u(w0|=¬ϕ)−},l w0∈W{R−(w,w0),→(w0|=¬ϕ)+}! ={definition of |=} G w0∈W{R−(w,w0)u(¬(w0|=ϕ))−},l w0∈W{R−(w,w0),→(¬(w0|=ϕ))+}! ={definition of ¬} G w0∈W{R−(w,w0)u(w0|=ϕ)+},l w0∈W{R−(w,w0),→(w0|=ϕ)−}! ={definition of 3 − ,} (3 − (w,ϕ,+),(w,ϕ,−)) ={definition of |=} (w|=/ 3ϕ) 4.2. Semantics and Satisfaction 53 (iv) / 3¬ϕ=/ϕ (w|=/ 3(¬ϕ)) ={definition of |=} G w0∈W{R−(w,w0)u(w0|=¬ϕ)+},l w0∈W{R−(w,w0),→(w0|=¬ϕ)−}! ={definition of |=} G w0∈W{R−(w,w0)u(¬(w0|=ϕ))+},l w0∈W{R−(w,w0),→(¬(w0|=ϕ))−}! ={definition of ¬} G w0∈W{R−(w,w0)u(w0|=ϕ)−},l w0∈W{R−(w,w0),→(w0|=ϕ)+}! ={definition of 3 − ,} (3 − (w,ϕ,−),(w,ϕ,+)) ={definition of |=} (w|=/ϕ) (v) (∼ϕ) = ∼(3ϕ) 54 Chapter 4. MIPL - A modal intuitionistic paraconsistent logic (w|= (∼ϕ)) ={definition of |=} l w0∈W{R+(w,w0),→(w0|=∼ϕ)+},G w0∈W{R+(w,w0)u(w0|=∼ϕ)−}! ={definition of |=} l w0∈W{R+(w,w0),→((w0|=ϕ) =⇒(0, 1))+},G w0∈W{R+(w,w0)u((w0|=¬ϕ) =⇒(0, 1))−}! ={definition of =⇒} l w0∈W{R+(w,w0),→((w0|=ϕ)+,→0)},G w0∈W{R+(w,w0)u(w0|=ϕ)+}! ={by Eq. (3)} l w0∈W{(R+(w,w0)u(w0|=ϕ)+),→0},G w0∈W{R+(w,w0)u(w0|=ϕ)+}! ={by Eq. (6) in Lemma 1} G w0∈W{(R+(w,w0)u(w0|=ϕ)+)},→0, G w0∈W{R+(w,w0)u(w0|=ϕ)+}! ={definition of 3 + } (3 + (w,ϕ,+) ,→0, 3 + (w,ϕ,+)) ={definition of =⇒} (3 + (w,ϕ,+),(w,ϕ,−)) =⇒(0, 1) ={definition of |=} (w|=3ϕ) =⇒(w|=⊥) ={definition of |=} (w|=∼(3ϕ)) (vi) /∼ϕ=¬∼/ 3ϕ 4.2. Semantics and Satisfaction 55 (w|=/(∼ϕ)) ={definition of |=} G w0∈W{R−(w,w0)u(w0|=∼ϕ)−},l w0∈W{R−(w,w0),→(w0|=∼ϕ)+}! ={definition of |=} G w0∈W{R−(w,w0)u((w0|=ϕ) =⇒(0, 1))−},l w0∈W{R−(w,w0),→((w0|=¬ϕ) =⇒(0, 1))+}! ={definition of =⇒} G w0∈W{R−(w,w0)u(w0|=ϕ)+},l w0∈W{R−(w,w0),→((w0|=ϕ)+,→0)}! ={by Eq. (3)} G w0∈W{R−(w,w0)u(w0|=ϕ)+},l w0∈W{(R−(w,w0)u(w0|=ϕ)+),→0}! ={by Eq. (6) in Lemma 1} G w0∈W{R−(w,w0)u(w0|=ϕ)+},(G w0∈W{R−(w,w0)u(w0|=ϕ)+}),→0! ={definition of 3 − } (3 − (w,ϕ,+),3 − (w,ϕ,+) ,→0) ={definition of ¬} ¬(3 − (w,ϕ,+) ,→0, 3 − (w,ϕ,+)) ={definition of =⇒} ¬((3 − (w,ϕ,+),(w,ϕ,−)) =⇒(0, 1)) ={definition of |=} ¬((w|=/ 3ϕ) =⇒(w|=⊥)) ={definition of |=} ¬(w|=∼(/ 3ϕ)) ={definition of |=} (w|=¬(∼(/ 3ϕ))) 56 Chapter 4. MIPL - A modal intuitionistic paraconsistent logic 4.3 modal preservations In this section we will define the notions of simulation and bisimulation between MIPL models and study the preservation of formulas between similar and bisimilar models. Consider two PLTS T1=hW1,R1i,T2=hW2,R2iand MIPL models M1= (T1,V1)and M2= (T2,V2)over Σ= (Π, Prop). Definition 25.A relation S⊆W1×W2is a simulation between MIPL models M1and M2if –Sis a simulation between PLTS T1and T2 – for any p∈Prop and hw,vi ∈ S,V1(w,p)4tV2(v,p) Lemma 7.If S ⊆W1×W2is a simulation between models M1and M2and hw,vi ∈ S then (w|=M1ϕ)4t(v|=M2ϕ)for ϕ∈Fm+3 where Fm+3is the positive fragment of MIPL with a single modal connective 3. Proof. In the proof the subscript of 4tis omitted and 4represents the truth ordering of A./. We consider as an induction hypothesis that for any ϕ,(w|=M1ϕ)4t(v|=M2ϕ). •if ϕ=> (w|=M1>) = (1, 0) = (v|=M2>) ∴(w|=M1>)4(v|=M2>) •if ϕ=⊥ (w|=M1⊥) = (0, 1) = (v|=M2⊥) ∴(w|=M1⊥)4(v|=M2⊥) •if ϕ=p:p∈Prop (w|=M1p)+ ={definition of |=} V+ 1(w,p) ≤ { definition of S} V+ 2(v,p) 4.3. Modal preservations 63 G w0∈W1{R− 1(w,w0)u(w0|=M1ϕ1)−} ≥ { monotonicity of t} G v0∈W2{R− 2(v,v0)u(v0|=M2ϕ1)−} ={definition of |=} (v|=M2/ϕ1)+ (w|=M1/ϕ1)− ={definition of |=} l w0∈W1{R− 1(w,w0),→(w0|=M1ϕ1)+} For any w0∈W1exists v0∈W2such that hw0,v0i ∈ S and R− 1(w,w0),→(w0|=M1ϕ1)+ ≤ { definition of S R− 1(w,w0)≥R− 2(v,v0)and by Eq. (2)} R− 2(v,v0),→(w0|=M1ϕ1)+ ≤ { Induction Hypothesis (w|=M1ϕ)+≤(v|=M2ϕ)+and by Eq. (1)} R− 2(v,v0),→(v0|=M2ϕ1)+ l w0∈W1{R− 1(w,w0),→(w0|=M1ϕ1)+} ≤ { monotonicity of u} l v0∈W2{R− 2(v,v0),→(v0|=M2ϕ1)+} ={definition of |=} (v|=M2/ϕ1)− 64 Chapter 4. MIPL - A modal intuitionistic paraconsistent logic ∴(w|=M1/ϕ1)/ 4(v|=M2/ϕ1) In fact, (v|=M2/ϕ)4(w|=M1/ϕ) •if ϕ=/ 3ϕ1 (w|=M1/ 3ϕ1)+ ={definition of |=} G w0∈W1{R− 1(w,w0)u(w0|=M1ϕ1)+} A counterexample using the G¨ odel algebra shows that (w|=M1/ 3ϕ1)+≤(v|=M2/ 3ϕ1)+is not necessarily true is the case where both worlds w and v have a single transition and where R− 1(w,w0) = 0.8 and R− 2(v,v0) = 0.6 (w0|=M1ϕ1)+=0.7 and (v0|=M2ϕ1)+=0.5 Here, R− 1(w,w0)u(w0|=M1ϕ1)+ ={-} 0.8 u0.7 ≥ { since 0.8 ≥0.6 and 0.7 ≥0.5 } 0.6 u0.5 ={definition of |=} R− 2(v,v0)u(v|=M2ϕ1)+ ∴(w|=M1/ 3ϕ1)/ 4(v|=M2/ 3ϕ1) Definition 26.A relation B⊆W1×W2is a bisimulation between MIPL models M1and M2 if –Bis a bisimulation between PLTS T1and T2 – for any p∈Prop and hw,vi ∈ B,V1(w,p) = V2(v,p). 4.3. Modal preservations 65 Theorem 3.Let B be a bisimulation between two MIPL models and hw,vi ∈ B. Then (w|=M1 ϕ) = (v|=M2ϕ)for ϕ∈Fm(Π,Prop). Proof. We consider as an induction hypothesis that for any ϕ,(w|=M1ϕ) = (v|=M2ϕ). •if ϕ=>(w|=M1>)+= (v|=M2>)+=1(w|=M1>)−= (v|=M2>)−=0 •if ϕ=⊥(w|=M1⊥)+= (v|=M2⊥)+=0(w|=M1⊥)−= (v|=M2⊥)−=1 •if ϕ=psuch that p∈Prop (w|=M1p) = V1(w,p) ={hw,vi ∈ B} (w|=M1p) = V2(v,p) ∴(w|=M1p) = (v|=M2p) •if ϕ=¬ϕ1 (w|=M1¬ϕ1) ={definition of |=} ((w|=M1ϕ1)−,(w|=M1ϕ1)+) ={Induction Hypothesis (w|=M1ϕ) = (v|=M2ϕ)} ((v|=M2ϕ1)−,(v|=M2ϕ1)+) ={definition of |=} (v|=M2¬ϕ1) ∴(w|=M1¬ϕ1) = (v|=M2¬ϕ1) •ϕ=ϕ1∧ϕ2 (w|=M1ϕ1∧ϕ2) ={definition of |=} (w|=M1ϕ1)∧ ∧(w|=M1ϕ2) ={Induction Hypothesis (w|=M1ϕ) = (v|=M2ϕ)} (v|=M2ϕ1)∧ ∧(v|=M2ϕ2) ={definition of |=} (v|=M2ϕ1∧ϕ2) ∴(w|=M1ϕ1∧ϕ2) = (v|=M2ϕ1∧ϕ2). 66 Chapter 4. MIPL - A modal intuitionistic paraconsistent logic •if ϕ=ϕ1∨ϕ2 (w|=M1ϕ1∨ϕ2) ={definition of |=} (w|=M1ϕ1)∨ ∨(w|=M1ϕ2) ={Induction Hypothesis (w|=M1ϕ) = (v|=M2ϕ)} (v|=M2ϕ1)∨ ∨(v|=M2ϕ2) ={definition of |=} (v|=M2ϕ1∨ϕ2) ∴(w|=M1ϕ1∨ϕ2) = (v|=M2ϕ1∨ϕ2). •if ϕ=ϕ1→ϕ2 (w|=M1ϕ1→ϕ2) ={definition of |=} (w|=M1ϕ1) =⇒(w|=M1ϕ2) ={Induction Hypothesis (w|=M1ϕ) = (v|=M2ϕ)} (v|=M2ϕ1) =⇒(v|=M2ϕ2) ={definition of |=} (v|=M2ϕ1→ϕ2) ∴(w|=M1ϕ1→ϕ2) = (v|=M2ϕ1→ϕ2) •if ϕ=3ϕ1 First note that any pair hw,viof a bisimulation between MIPL models satisfies the following condition: –∀w0∈W1∃v0∈W2such that R+ 1(w,w0) = R+ 2(v,v0),R− 1(w,w0) = R− 2(v,v0)and hw0,v0i ∈ B.(∗) This follows directly from the definition of bisimulation between two PLTS. 4.3. Modal preservations 67 (w|=M13ϕ1)+ ={definition of |=} G w0∈W1 (R+ 1(w,w0)u(w0|=M1ϕ1)+) ={by (∗)and Induction Hypothesis (w|=M1ϕ) = (v|=M2ϕ)} G w0∈W1 (R+ 2(v,v0)u(v0|=M2ϕ1)+) ={definition of |=} (v|=M23ϕ1)+ (w|=M13ϕ1)− ={definition of |=} l w0∈W1 (R+ 1(w,w0),→(w0|=M1ϕ)−) ={by (∗)and Induction Hypothesis (w|=M1ϕ) = (v|=M2ϕ)} l v0∈W1 (R+ 2(v,v0),→(v0|=M2ϕ)−) ={definition of |=} (v|=M23ϕ1)− ∴(w|=M13ϕ1) = (v|=M23ϕ1). •if ϕ=ϕ1 68 Chapter 4. MIPL - A modal intuitionistic paraconsistent logic (w|=M1ϕ1) ={definition of |=} (l w0∈W1 (R+ 1(w,w0),→(w0|=M1ϕ1)+),G w0∈W1 (R+ 1(w,w0)u(w0|=ϕ1)−)) ={by (∗)and Induction Hypothesis (w|=M1ϕ) = (v|=M2ϕ)} (l v0∈W2 (R+ 2(v,v0),→(v0|=M2ϕ1)+),G v0∈V1 (R+ 2(v,v0)u(v0|=M2ϕ1)−)) ={definition of |=} (v|=M2ϕ1) ∴(w|=M1ϕ1) = (v|=M2ϕ1) •if ϕ=/ϕ1 (w|=M1/ϕ1) ={definition of |=} (G w0∈W1 (R− 1(w,w0)u(w0|=M1ϕ1)−),l w0∈W1 (R− 1(w,w0)→(w0|=M1ϕ1)+)) ={by (∗)16 and Induction Hypothesis (w|=M1ϕ) = (v|=M2ϕ)} (G v∈W2 (R− 2(v,v0)u(v0|=M2ϕ1)−),l v∈W2 (R− 2(v,v0),→(v0|=M2ϕ1)+)) ={definition of |=} (v|=M2/ϕ1) ∴(w|=M1/ϕ1) = (v|=M2/ϕ1) 4.3. Modal preservations 69 •if ϕ=/ 3ϕ1 (w|=M1/ 3ϕ1) ={definition of |=} (G w0∈W1 (R− 1(w,w0)u(w0|=M1ϕ1)+),l w0∈W1 (R− 1(w,w0),→(w0|=M1ϕ1)−)) ={by (∗)16 and Induction Hypothesis (w|=M1ϕ) = (v|=M2ϕ)} (G v∈W2 (R− 2(v,v0)u(v0|=M2ϕ1)+),l v∈W2 (R− 2(v,v0),→(v0|=M2ϕ1)−)) ={definition of |=} (v|=M2/ 3ϕ1) ∴(w|=M1/ 3ϕ1) = (v|=M2/ 3ϕ1) 5 CONCLUSION 5.1 summary of contributions In this work we have proposed a new family of transition systems, the Paraconsistent Labelled Transition Systems, also written PLTS, whose transitions are described by two fuzzy relations, besides the usual labelling action. These transition systems are suited to model any dynamic process where there is some kind of contradiction or lack of information regarding the existence of transitions between states, also supporting consistent scenarios. We have established different forms of equivalence between PLTS, given by the definition of morphism, simulation and bisimulation. We also developed the notion of equivalence between states with the definition of traces and trace equivalence. Motivated by the possible use of PLTS as a model for quantum computation, illustrated below, we defined a category of PLTS and their morphisms, which we endowed with constructions that could serve as a basis for the definition of a process algebra and thus as a possible formalism for parallel quantum computations. We have proposed a modal intuitionistic paraconsistent logic, MIPL, whose semantic models are defined over PLTS. The valuation of propositions and the satisfaction of formulas in MIPL model the lack and excess of information, besides consistent valuations. MIPL supports inconsistency and vagueness both at the level of the accessibility relations in its underlying relational structure and at the level of proposition variables. Given some process modeled by a PLTS, MIPL is a tool for talking about its properties as well as to compare the satisfaction of formulas in models related by the equivalence notions mentioned above. 5.2 modeling quantum circuits -an application of plts Quantum circuits (QC) are a promising model for quantum computing, but superconducting qubits may hold in a superposition state for a limited period of time, i.e. the coherence time. Decoherence consists in decay of a qubit in superposition to its ground state and may be caused by distinct physical phenomena, each with a certain probability of occurring. A 72 Chapter 5. Conclusion quantum circuit is effective only if gate operations and measurements are performed to superposition states within a limited period of time after their preparation. When that time is exceeded there is an increasing probability that the circuit does not behave according to its design, since there may be decayed states in place of superposition states. One approach to solve this problem is to enhance superconducting qubits performance, increasing their coherence time. If the coherence time is large enough to ensure that no decay will occur over the time the circuit is being executed, decoherence is no longer an error factor to quantum computations. Here we do not explore this possibility. Instead, we provide a model for quantum circuits which incorporates the possible decoherence of state of the art superconducting qubits as an error factor. This way, quantum circuits are translated into a structure which models not only the desired computation but the behavior of the circuit when executed in a real setting. 5.2.1From quantum circuits to PLTS We will use PLTS to model quantum circuits, taking advantage of their accessibility relations in the following way. Coherence of qubits is not an exact measure, but usually given by a time interval. This fixes two values of coherence, corresponding to a worst case scenario and a best case scenario. We employ the two accessibility relations in a PLTS to model both scenarios simultaneously. Other important observation for the conversion of quantum circuits to PLTS is that quantum circuits always have a sequential execution. Simultaneous operations performed to distinct qubits are combined using the tensor product construction ⊗into a single operation to the whole collection of qubits treated by the circuit. Thus a quantum circuit may be described by a sequence of executions e1,e2,e3, ... where each eiis the tensor product of the operations performed to the qubits at each execution step. Starting from the initial state where, for instance, all qubits are in the state |0i, each eitakes the collection of qubits to a new state, specified by the state of each qubit after eiis performed. Example 17.Consider, for instance, the following circuit designed with IBM Quantum Composer, an online tool for designing and testing quantum circuits. It is a simple circuit which creates a superposition state in a qubit resister, with the application of the Hadamard gate, and after performs a measurement to that qubit. 5.3. Prospect for future work 79 and the value for the negative accessibility relation as r−=   1 if Wn i=1{P− i} ≥ 1 Wn i=1{P− i}otherwise 5.3 prospect for future work Enrich MIPL with a consistency connective In the same way the conflation operation was used to determine if a particular transition of an A-PLTS, where Ais an MTL-algebra over [0, 1], was within the intuitionistic, strictly consistent or paraconsistent domain, it could be used to determine the consistency of formulas in an MIPL model over a such a PLTS. A formula ϕis considered consistent if the evidence of it being true and the evidence of it being false are non-contradictory, which in the fuzzy framework means they add to 1 or to a value less than 1. In other words, if the satisfaction of ϕis given by the pair (a,b),ϕis consistent only if (a,b)≤a(a,b)where a is, as before, the conflation operation. In light of this consideration, we could extend MIPL grammar with a consistency connective ◦and define the satisfaction of a formula ◦ϕin a world wof an MIPL model over an A-PLTS as follows. (w|=◦ϕ) =    (1, 0)iff (a,b)≤a(a,b) (0, 1)otherwise Another possibility is to endow the underlying MTL-algebra of a PLTS with the structure of a metric space and a notion of distance. Definition 27. A =hA,u,t,1,0,,→,diis a metric MTL-algebra if 1.A=hA,u,t,1,0,,→i in an MTL-algebra, and 2.(A,d)is a metric space, that is, for any x,y,z∈A,d:A×A→R+ 0is such that: –d(x,y) = 0 iff x=y –d(x,y)≤d(x,z) + d(z,y) Moreover, we can define a bilattice over Aand a distance metric D:(A×A)×(A×A)→ R+ 0over bilattice pairs. For instance, for any (a,b),(c,d)∈A×Awe could have D((a,b),(c,d)) = qd(a,c)2+d(c,d)2 or D((a,b),(c,d)) = d(a,c) + d(c,d) 80 Chapter 5. Conclusion In this way we could define the sets of intuitionistic and paraconsistent pairs, ∆P,∆I, respectively, as ∆I={(a,b)|D((a,b),(0, 0)) ≤D((a,b),(1, 1))} ∆P={(a,b)|D((a,b),(1, 1)) ≤D((a,b),(0, 0))} Then, it is possible to establish if a bilattice element (a,b)represents incomplete or contradictory information by comparing its distance to the elements (0, 0)and (1, 1). Moreover, the bilattice elements equally distant from (0, 0)and (1, 1)are those representing complete information, lying in the set of strictly consistent pairs ∆, formally defined as ∆=∆P∩∆I A formula in MIPL is consistent when its satisfaction is given by (a,b)such that (a,b)∈ ∆I(note that ∆⊂∆I); it is inconsistent when (a,b)∈∆P\∆. Thus satisfaction of a formula ◦ϕin a world wof a MIPL model over a metric MTL-PLTS would be defined as (w|=◦ϕ) =    (1, 0)iff (w|=ϕ)∈∆I (0, 1)otherwise Develop a process language and design a dynamic extension of MIPL The constructions defined in Chapter 3could be explored to develop a process language. Having programs described by PLTS, as, for instance, quantum circuit executions, such a language would allow to represent parallel executions of those programs. Following this line of work, the next step would be to extend MIPL to a dynamic logic. Improve the description of quantum circuits as PLTS Finally, it would be interesting to further explore the description of quantum circuits as PLTS and improve the method described above for this conversion. The notions of simulation and bisimulation fail to describe the equivalence of circuits in the examples above, so one needs to study how to better characterize suitable mappings between PLTS. If the conversion from QC to PLTS is worthwhile in the engineering of quantum software, it is possible to design a tool for representing classes of equivalent quantum algorithms and to define metrics of quality, establishing which circuit implementation better performs a given algorithm. BIBLIOGRAPHY [BEGR09] F´ elix Bou, Francesc Esteva, Llu´ ıs Godo, and Ricardo Oscar Rodr´ ıguez. On the Minimum Many-Valued Modal Logic over a Finite Residuated Lattice. Journal of Logic and Computation,21(5):739–790,10 2009. [Bel77] Nuel Belnap. A useful four-valued logic. 1977. [BS11] Alexandru Baltag and Sonja Smets. Quantum logic as a dynamic logic. Synthese, 179(2):285–306,2011. [BvN37] Garrett Birkhoff and John von Neumann. The logic of quantum mechanics. Journal of Symbolic Logic,2(1):44–45,1937. [CCM07] Walter Carnielli, Marcelo E. Coniglio, and Jo˜ ao Marcos. Logics of Formal Inconsistency. Handbook of Philosophical Logic, pages 1–93,2007. [Com98] Stephen D. Comer. Paul halmos and steven givant. logic as algebra. the dolciani mathematical expositions, no. 21. the mathematical association of america, washington 1998, ix 141 pp. Journal of Symbolic Logic,63(4):1604–1604,1998. [EG01] Francesc Esteva and Lluis Godo. Godo, l.: Monoidal t-norm based logic: Towards a logic for left-continuous t-norms. fuzzy sets and systems 124(3), 271-288. Fuzzy Sets and Systems,124:271–288,12 2001. [Fit89] Melvin Fitting. Bilattices and the theory of truth. Journal of Philosophical Logic, 18(3):225–256,1989. [Flo67] Robert W. Floyd. Assigning meanings to programs. Mathematical aspects of computer science,19(19-32):1,1967. [Gin86] Matthew L. Ginsberg. Multi-valued logics. In Proceedings of the Fifth AAAI National Conference on Artificial Intelligence, AAAI’86, pages 243–247. AAAI Press, 1986. [Gin88] Matthew Ginsberg. Multivalued logics: A uniform approach to reasoning in ai. Computer Intelligence,4(1):256–316,1988. [Hoa69] C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576–580, October 1969. 82 bibliography [HTK00] David Harel, Jerzy Tiuryn, and Dexter Kozen. Dynamic Logic. MIT Press, Cambridge, MA, USA, 2000. [Ja´ s69a] Stanisław Ja´ skowski. Propositional calculus for contradictory deductive systems. Studia Logica,24(1):143–157,1969. [Ja´ s69b] Stanisław Ja´ skowski. Propositional calculus for contradictory deductive systems. Studia Logica,24(1):143–157,1969. [Kel76] Robert Keller. Formal verification of parallel programs. Commun. ACM,19:371– 384,07 1976. [Koz85] Dexter Kozen. A probabilistic pdl. Journal of Computer and System Sciences, 30(2):162–178,1985. [Kra98] Marcus Kracht. On extensions of intermediate logics by strong negation. Journal of Philosophical Logic,27(1):49–73,1998. [KS14] Sofia Kouah and Djamel Eddine Saidouni. Fuzzy labeled transition refinement tree: Application to stepwise designing multi agent systems. International Journal of Agent Technologies and Systems,6:1–31,07 2014. [LL34] C. I. Lewis and C. H. Langford. Symbolic logic. Erkenntnis,4(1):65–66,1934. [LS91] Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. Information and Computation,94(1):1–28,1991. [MN04] Erik Meineche Schmidts Mikkel Nygaard. DAIMI FN : Transition systems : algorithms and data structures. Matematisk Institut, Aarhus Universitet, Datalogisk Afdeling, Aarhus, 2004. [MNM16] Alexandre Madeira, Renato Neves, and Manuel A. Martins. An exercise on the generation of many-valued dynamic logics. Journal of Logical and Algebraic Methods in Programming,85(5, Part 2):1011–1037,2016. Articles dedicated to Prof. J. N. Oliveira on the occasion of his 60th birthday. [NC11] Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press, USA, 10th edition, 2011. [OW10] Sergei P. Odintsov and Heinrich Wansing. Modal logics with belnapian truth values. Journal of Applied Non-Classical Logics,20(3):279–301,2010. [PBW18] Graham Priest, Francesco Berto, and Zach Weber. Dialetheism. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Fall 2018 edition, 2018. bibliography 83 [Pla10] Andr Platzer. Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer Publishing Company, Incorporated, 1st edition, 2010. [Plo04] Gordon Plotkin. A structural approach to operational semantics. J. Log. Algebr. Program.,60-61:17–139,07 2004. [Pre18] John Preskill. Quantum computing in the nisq era and beyond. Quantum,2:79, Aug 2018. [RJJ15] Umberto Rivieccio, Achim Jung, and Ramon Jansana. Four-valued modal logic: Kripke semantics and duality. Journal of Logic and Computation,27(1):155–199,06 2015. [Sed16] Igor Sedl´ ar. Propositional dynamic logic with belnapian truth values. 08 2016. [Usp92] Vladimir A. Uspensky. Kolmogorov and mathematical logic. Journal of Symbolic Logic,57(2):385–412,1992. [Vak77] D. Vakarelov. Notes on n-lattices and constructive logic with strong negation. Studia Logica,36(1):109–125,1977. [vAS15] Mark van Atten and G¨ oran Sundholm. L.e.j. brouwer’s ‘unreliability of the logical principles’. a new translation, with an introduction, 11 2015. [WD38] Morgan Ward and R. P. Dilworth. Residuated lattices. Proceedings of the National Academy of Sciences of the United States of America,24(3):162–164,1938. [WN95] Glynn Winskel and Mogens Nielsen. Models for Concurrency, pages 1–148. Oxford University Press, Inc., USA, 1995. [ZDL+19] Yu Zhang, Haowei Deng, Quanxi Li, Haoze Song, and Leihai Nie. Optimizing quantum programs against decoherence: Delaying qubits into quantum superposition. 2019 International Symposium on Theoretical Aspects of Software Engineering (TASE), Jul 2019. A SUPPORT MATERIAL Auxiliary results which are not main-stream; or Details of results whose length would compromise readability of main text; or Specifications and Code Listings: should this be the case; or Tooling: Should this be the case. NB: place here information about funding, FCT project, etc in which the work is framed. Leave empty otherwise.