Maximizing the Number of Visible Labels on a Rotating Map

For a map that can be rotated, we consider the following problem. There are a number of feature points on the map, each having a geometric object as a label. The goal is to find the largest subset of these labels such that when the map is rotated and the labels remain vertical, no two labels in the subset intersect. We show that, even if the labels are vertical bars of zero width, this problem remains NP-hard, and present a polynomial approximation scheme for solving it. We also introduce a new variant of the problem for vertical labels of zero width, in which any label that does not appear in the output must be coalesced with a label that does. Coalescing a subset of the labels means to choose a representative among them and set its label height to the sum of the individual label heights.

On Quantum-MV Algebras - Part I: The Orthomodular Algebras

We prove that almost all the properties of quantum-MV algebras are verified by orthomodular algebras, the new algebras introduced in a previous paper. We put a special insight on transitive antisymmetric orthomodular (taOM) algebras, generalizations of MV algebras. We make the connection with IMTL and NM algebras. In memoriam Dragos. Vaida (1933 – 2020)

Topological Characterization of the Third Type of Triangular Hex-derived Networks

A topological index is a numerical quantity that defines a chemical descriptor to report several physical, biological and chemical properties of a chemical structure. In recent literature, various degree-based topological indices of a molecular structure are easily calculated by deriving a M-polynomial of that structure. In this paper, we first determine the expression of a M-polynomial of the triangular Hex-derived network of type three of dimension n and then obtain the corresponding degree-based topological indices from the closed form of M-polynomial. In addition, we use Maple software to represent the M-polynomial and the concerned degree-based topological indices pictorially for different dimensions.

A Translation of Weighted LTL Formulas to Weighted Buchi Automata over omega-valuation Monoids

In this paper we introduce a weighted LTL over product omega-valuation monoids that satisfy specific properties. We also introduce weighted generalized Buchi automata with epsilon-transitions, as well as weighted Buchi automata with epsilon-transitions over product omega-valuation monoids and prove that these two models are expressively equivalent and also equivalent to weighted Buchi automata already introduced in the literature. We prove that every formula of a syntactic fragment of our logic can be effectively translated to a weighted generalized Buchi automaton with epsilon-transitions. For generalized product omega-valuation monoids that satisfy specific properties we define a weighted LTL, weighted generalized Buchi automata with epsilon-transitions, and weighted Buchi automata with epsilon-transitions, and we prove the aforementioned results for generalized product omega-valuation monoids as well. The translation of weighted LTL formulas to weighted generalized Buchi automata with epsilon-transitions is now obtained for a restricted syntactical fragment of the logic.

Qualifications of Instruction Sequence Failures, Faults and Defects: Dormant, Effective, Detected, Temporary, and Permanent

Starting out from the survey of instruction sequence faults from [6] program faults are classified according to the conventional criteria of being dormant, effective, detected, temporary, and permanent. Being retrospectively approved is introduced as an additional qualification. For this theoretical investigation the context is simplified by contemplating instruction sequences as a theoretical model for programs, and by assuming that instruction sequences are supposed to compute total transformations on finite bit sequences of a fixed length only. The main conclusion which can be drawn from this work concerns the notion of dormancy. First of all it is noticed that the unconventional notion of a dormant failure is both plausible and amenable to a straightforward and convincing definition. The conventional notion of a dormant fault, however, is much harder to grasp and the definition of a dormant fault which is provided in the paper may be disputed. The notion of a dormant fault seems to admit no convincing intuition. All faults are defects but not the other way around. The idea of a fault exclusively depends on an instruction sequence and a specification of which it is considered to be a candidate implementation. In the presence of a design, however, in addition to faults, the notion of a deviation from design (DFD) defect arises, which constitutes a class of defects many of which are not faults. For DFD defects the notion of dormancy admits a straightforward and convincing definition.

Applying MDE to ROS Systems: A Comparative Analysis

The Robot Operating System (ROS) is one of the most used software framework to develop robot applications. Although it is possible to reuse packages and code from other ROS projects, ROS applications remain low level and reasoning at a higher level of abstraction is not possible. Using Model-Driven Engineering (MDE) in the context of ROS applications would allow to increase the accessibility of ROS, leverage the reusability of packages and supply validation of the software earlier in the design, using formal methods. For instance, formal verification methods would improve the overall dependability of robotic systems. Our view is that we should increase the abstraction of the systems through models using MDE methodology in order to enable the use of formal methods on ROS applications. In this paper we do a first step toward this and propose a comparative study of existing modeling alternatives aiming to help roboticists to smoothly adopt MDE. This study compares the use of modeling in ROS systems in three different ways: by means of direct UML modeling, a ROS UML profile and a ROS Domain-Specific Language. That allows us to pick the solution that better fits our needs.

Small Longest Tandem Scattered Subsequences

We consider the problem of identifying tandem scattered subsequences within a string. Our algorithm identifies a longest subsequence which occurs twice without overlap in a string. This algorithm is based on the Hunt-Szymanski algorithm, therefore its performance improves if the string is not self similar, which occurs naturally on strings over large alphabets. Our algorithm relies on new results for data structures that support dynamic longest increasing sub-sequences. In the process we also obtain improved algorithms for the decremental string comparison problem.

A Note on Congruences of Infinite Bounded Involution Lattices

We prove that an infinite (bounded) involution lattice and even pseudo-Kleene algebra can have any number of congruences between 2 and its number of elements or equalling its number of subsets, regardless of whether it has as many ideals as elements or as many ideals as subsets. Furthermore, when they have at most as many congruences as elements, these involution lattices and even pseudo-Kleene algebras can be chosen such that all their lattice congruences preserve their involutions, so that they have as many congruences as their lattice reducts. Under the Generalized Continuum Hypothesis, this means that an infinite (bounded) involution lattice and even pseudo-Kleene algebra can have any number of congruences between 2 and its number of subsets, regardless of its number of ideals. Consequently, the same holds for antiortholattices, a class of paraorthomodular Brouwer-Zadeh lattices. Regarding the shapes of the congruence lattices of the lattice{ ordered algebras in question, it turns out that, as long as the number of congruences is not strictly larger than the number of elements, they can be isomorphic to any nonsingleton well-ordered set with a largest element of any of those cardinalities, provided its largest element is strictly join-irreducible in the case of bounded lattice-ordered algebras and, in the case of antiortholattices with at least 3 distinct elements, provided that the predecessor of the largest element of that well-ordered set is strictly join{irreducible, as well; of course, various constructions can be applied to these algebras to obtain congruence lattices with different structures without changing the cardinalities in question. We point out sufficient conditions for analogous results to hold in an arbitrary variety.

Sumterms, Summands, Sumtuples, and Sums and the Meta-Arithmetic of Summation

Sumterms are introduced as syntactic entities, and sumtuples are introduced as semantic entities. Equipped with these concepts a new description is obtained of the notion of a sum as (the name for) a role which can be played by a number. Sumterm splitting operators are introduced and it is argued that without further precautions the presence of these operators gives rise to an instance of the so-called sum splitting paradox. A survey of solutions to the sum splitting paradox is given.

Instruction Sequence Faults with Formal Change Justification

The notion of an instruction sequence fault is considered as a theoretical concept, for which the justification of the qualification of a fragment as faulty is mathematical instead of pragmatic, the latter approach being much more common. Starting from so-called Laski faults a range of patterns of faults and changes thereof for instruction sequences is developed.