A Weakness Measure for GR(1) Formulae

When dealing with unrealizable specifications in reactive synthesis, finding the weakest environment assumptions that ensure realizability is often considered a desirable property. However, little effort has been dedicated to defining or evaluating the notion of weakness of assumptions formally. The question of whether one assumption is weaker than another is commonly interpreted by considering the implication relationship between the two or, equivalently, their language inclusion. This interpretation fails to provide any insight into the weakness of the assumptions when implication (or language inclusion) does not hold. To our knowledge, the only measure that is capable of comparing two formulae in this case is entropy, but even it cannot distinguish the weakness of assumptions expressed as fairness properties. In this paper, we propose a refined measure of weakness based on combining entropy with Hausdorff dimension, a concept that captures the notion of size of the $$\omega $$ ω -language satisfying a linear temporal logic formula. We focus on a special subset of linear temporal logic formulae which is of particular interest in reactive synthesis, called GR(1). We identify the conditions under which this measure is guaranteed to distinguish between weaker and stronger GR(1) formulae, and propose a refined measure to cover cases when two formulae are strictly ordered by implication but have the same entropy and Hausdorff dimension. We prove the consistency between our weakness measure and logical implication, that is, if one formula implies another, the latter is weaker than the former according to our measure. We evaluate our proposed weakness measure in two contexts. The first is in computing GR(1) assumption refinements where our weakness measure is used as a heuristic to drive the refinement search towards weaker solutions. The second is in the context of quantitative model checking where it is used to measure the size of the language of a model violating a linear temporal logic formula.

Computation Tree Logic Formula Model Checking Using DNA Computing

Computation tree logic model checking is a formal verification technology that can ensure the correctness of systems. The vast storage density of deoxyribonucleic acid (DNA) molecules and the massive parallelism of DNA computing offer new methods for computation tree logic model checking. In this study, we propose a computation tree logic model checking method based on DNA computing. First, a system to-be-checked and a computation tree logic formula are encoded by single-stranded DNA molecules. Second, these singlestranded DNA molecules are mixed to spontaneously hybridize and form partial or complete double-stranded molecules. Finally, a series of molecular manipulations are applied to detect the double-stranded molecules so that the result whether the system satisfies the computation tree logic formula is obtained. Biological simulations confirm the validity of the new method.

Jauch–Piron states on quantum logics

We show in this note that if [Formula: see text] is a Boolean subalgebra of the lattice quantum logic [Formula: see text], then each state on [Formula: see text] can be extended over [Formula: see text] as a Jauch–Piron state provided [Formula: see text] is Jauch–Piron unital with respect to [Formula: see text] (i.e. for each nonzero [Formula: see text], there is a Jauch–Piron state [Formula: see text] on [Formula: see text] such that [Formula: see text]). We then discuss this result for the case of [Formula: see text] being the Hilbert space logic [Formula: see text] and [Formula: see text] being a set-representable logic.

Tu-vera

This article describes how the encryption algorithm (called Tu-vera) depends on the transformation of a phrase written in English into a sequence of propositional logic formulas which can be understand by a human receiver. This happens if the receiver has a set of reserved words and he/she knows the level of unfolding manipulation that the receiver needs to perform in the transformation of the phrase/sentence. The Tu-vera algorithm requires several steps like a) to give a phrase; b) to re-order words of the given phrase in order to form a propositional logic formula; c) to make use of background knowledge by performing substitutions; d) to answer questions in general subjects (like literature, biology and so forth); e) to change synonyms/antonyms (if this is feasible); f) to perform actions in order to give value to both or one operand of the logic formula and g) to conclude the final answer of the logic formula (true or false) depending of the logic values of the operands in the logic formula. Finally, a working example, in the subject of universal history is introduced.

Basic Logic, SMT solvers and finitely generated varieties of GBL-algebras

We show how to implement an effective decision procedure to check if a propositional Basic Logic formula is a tautology. For a formula with $n$ variables, the procedure consists of a translation, depending on $n$, from Basic Logic to the language of Satisfiability Modulo Theories SMT-LIB2 using the theory of quantifier free linear real arithmetic. Many efficient SMT-solvers exist to decide formulas in the SMT-LIB2 language. We also study finitely generated varieties of Basic Logic (BL-)algebras and give a description of the lattice of these varieties. Extensions to finitely generated varieties of Generalized BL-algebras are discussed, and a simple connection between finite GBL-algebras and finite closure algebras is noted.

Methodology for the Elaboration of Quizzes using Propositional Logic Calculus in an E-Learning Environment

This paper introduces the use of propositional logic calculus in the elaboration of educational quizzes to assess the level understanding of students in a specific theme of their courses. The technique introduced in this paper goes beyond multiple-choice quizzes. The technique requires several steps like a) to give a phrase, b) to re-order words of the given phrase in order to form a propositional logic formula, c) to make use of background knowledge for performing substitutions, d) to answer questions from one of the person in the team, e) to change synonyms/antonyms (if this is feasible), f) to perform actions in order to give value to both or at least one operand of the logic formula and g) to conclude the final answer of the logic formula (true or false) depending of the logic values of the operands in the logic formula. As a working example, the author shows a quiz for universal history, however, the same technique could be used to assess students in different courses.