FORMAL DESCRIPTIONS OF CODE PROPERTIES: DECIDABILITY, COMPLEXITY, IMPLEMENTATION

2012 ◽  
Vol 23 (01) ◽  
pp. 67-85 ◽  
Author(s):  
KRYSTIAN DUDZINSKI ◽  
STAVROS KONSTANTINIDIS
Keyword(s):  
Formal Methods ◽  
Coding Theory ◽  
Regular Language ◽  
Formal Method ◽  
Formal Languages ◽  
Decision Procedures ◽  
Regular Languages ◽  
Formal Expression ◽  
Initial Implementation ◽  
Code Property

The branch of coding theory that is based on formal languages has produced several methods for defining code properties, including word relations, dependence systems, implicational conditions, trajectories, and language inequations. Of those, the latter three can be viewed as formal methods in the sense that a certain formal expression can be used to denote a code property. Here we present a formal method which is based on transducers. Each transducer of a certain type defines/describes a desired code property. The method provides simple and uniform decision procedures for the basic questions of property satisfaction and maximality for regular languages. Our work includes statements about the hardness of deciding some of the problems involved. It turns out that maximality can be hard to decide even for "classical" code properties of finite languages. We also present an initial implementation of a LAnguage SERver capable of deciding the satisfaction problem for a given transducer code property and regular language.

scholarly journals Design of Formal Languages and Interfaces

2014 ◽  
pp. 301-314 ◽  
Author(s):  
Maria Spichkova
Keyword(s):  
Formal Methods ◽  
Development Process ◽  
Formal Method ◽  
System Development ◽  
Formal Languages ◽  
Point Of View ◽  
Tool Support ◽  
Mathematical Point ◽  
Two Factors ◽  
Engineering Psychology

This chapter provides an introduction to a work that aims to apply the achievements of engineering psychology to the area of formal methods, focusing on the specification phase of a system development process. Formal methods often assume that only two factors should be satisfied: the method must be sound and give such a representation, which is concise and beautiful from the mathematical point of view, without taking into account any question of readability, usability, or tool support. This leads to the fact that formal methods are treated by most engineers as something that is theoretically important but practically too hard to understand and to use, where even some small changes of a formal method can make it more understandable and usable for an average engineer.

Specifying with Interface and Trait Abstractions in Abstract State Machines: A Controlled Experiment

2021 ◽  
Vol 30 (4) ◽  
pp. 1-29
Author(s):  
Philipp Paulweber ◽  
Georg Simhandl ◽  
Uwe Zdun
Keyword(s):  
Formal Methods ◽  
Formal Method ◽  
Object Oriented ◽  
Controlled Experiment ◽  
Specification Languages ◽  
Randomized Design ◽  
Textual Description ◽  
Efficiency And Effectiveness ◽  
Completely Randomized Design ◽  
Experimental Group

Abstract State Machine (ASM) theory is a well-known state-based formal method. As in other state-based formal methods, the proposed specification languages for ASMs still lack easy-to-comprehend abstractions to express structural and behavioral aspects of specifications. Our goal is to investigate object-oriented abstractions such as interfaces and traits for ASM-based specification languages. We report on a controlled experiment with 98 participants to study the specification efficiency and effectiveness in which participants needed to comprehend an informal specification as problem (stimulus) in form of a textual description and express a corresponding solution in form of a textual ASM specification using either interface or trait syntax extensions. The study was carried out with a completely randomized design and one alternative (interface or trait) per experimental group. The results indicate that specification effectiveness of the traits experiment group shows a better performance compared to the interfaces experiment group, but specification efficiency shows no statistically significant differences. To the best of our knowledge, this is the first empirical study studying the specification effectiveness and efficiency of object-oriented abstractions in the context of formal methods.

Further Remarks on the Operational Nonterminal Complexity

2021 ◽  
pp. 1-15
Author(s):  
Jürgen Dassow
Keyword(s):  
Regular Language ◽  
Regular Languages ◽  
Partial Result ◽  
Natural Numbers ◽  
Left Quotient

For a regular language [Formula: see text], let [Formula: see text] be the minimal number of nonterminals necessary to generate [Formula: see text] by right linear grammars. Moreover, for natural numbers [Formula: see text] and an [Formula: see text]-ary regularity preserving operation [Formula: see text], let the range [Formula: see text] be the set of all numbers [Formula: see text] such that there are regular languages [Formula: see text] with [Formula: see text] for [Formula: see text] and [Formula: see text]. We show that, for the circular shift operation [Formula: see text], [Formula: see text] is infinite for all [Formula: see text], and we completely determine the set [Formula: see text]. Moreover, we give a precise range for the left right quotient and a partial result for the left quotient. Furthermore, we add some values to the range for the operation intersection which improves the result of [2].

Towards the Integration of a Formal Object-Oriented Method and Relational Unified Process

2011 ◽  
pp. 101-133
Author(s):  
Jing Liu ◽  
Zhiming Lui ◽  
Xiaoshan Li ◽  
He Jifend ◽  
Yifeng Chen
Keyword(s):  
Formal Methods ◽  
Formal Method ◽  
System Development ◽  
Scale Up ◽  
Object Oriented ◽  
Use Case ◽  
Object Oriented Method ◽  
Unified Process ◽  
Sound Foundation

In this chapter, we study the use of a formal object-oriented method within Relational Unified Process (RUP). Our purposes are (a) to unify different views of UML models; (b) to enhance RUP and UML with a formal method to improve the quality of software; (c) to scale up the use of the formal method with the use-case driven, iterative and incremental aspects of RUP. Our overall aim is to establish a sound foundation of RUP and UML and scale up the use of formal methods in software-intensive system development.

Rough Fuzzy Automata and Rough Fuzzy Grammar

2017 ◽  
Vol 6 (1) ◽  
pp. 36-55 ◽  
Author(s):  
Kanchan Tyagi ◽  
Alka Tripathi
Keyword(s):  
Regular Language ◽  
Formal Languages ◽  
Automata Theory ◽  
Formal Grammar ◽  
Computational Theory ◽  
Fuzzy Automata ◽  
Definition Of

Automata theory plays a key role in computational theory as many computational problems can be solved with its help. Formal grammar is a special type of automata designed for linguistic purposes. Formal grammar generates formal languages. Rough grammar and rough languages were introduced to incorporate the imprecision of real languages in formal languages. These languages have limitations on uncertainty. The authors have considered both uncertainty and approximations to define rough fuzzy grammar and rough fuzzy languages. Under certain restrictions, their grammar reduces to formal grammar. Furthermore, the authors have proposed definition of rough fuzzy automata that accepts rough fuzzy regular language.

scholarly journals BOND-FREE LANGUAGES: FORMALIZATIONS, MAXIMALITY AND CONSTRUCTION METHODS

2005 ◽  
Vol 16 (05) ◽  
pp. 1039-1070 ◽  
Author(s):  
LILA KARI ◽  
STAVROS KONSTANTINIDIS ◽  
PETR SOSÍK
Keyword(s):  
Polynomial Time ◽  
Structural Characterization ◽  
Regular Languages ◽  
Important Case ◽  
Similarity Relation ◽  
Construction Methods ◽  
Large Sets ◽  
Code Property ◽  
Context Free

The problem of negative design of DNA languages is addressed, that is, properties and construction methods of large sets of words that prevent undesired bonds when used in DNA computations. We recall a few existing formalizations of the problem and then define the property of sim-bond-freedom, where sim is a similarity relation between words. We show that this property is decidable for context-free languages and polynomial-time decidable for regular languages. The maximality of this property also turns out to be decidable for regular languages and polynomial-time decidable for an important case of the Hamming similarity. Then we consider various construction methods for Hamming bond-free languages, including the recently introduced method of templates, and obtain a complete structural characterization of all maximal Hamming bond-free languages. This result is applicable to the θ-k-code property introduced by Jonoska and Mahalingam.

Utilization of Concept Selection Methods: A Survey of Finnish Industry

2005 ◽  
Author(s):  
Mikko Salonen ◽  
Matti Perttula
Keyword(s):  
Formal Methods ◽  
Design Research ◽  
Formal Method ◽  
Formal Concept ◽  
Concept Design ◽  
Selection Methods ◽  
Concept Selection ◽  
Analytic Hierarchy ◽  
Industrial Utilization ◽  
Concept Review

Concept selection is an area of design research that has been under considerable interest over the years. There is, however, only little information on how the methods that have been presented in design research for this task have been adopted by industry. Thus, a survey was carried out in the Finnish industry. The results revealed that the degree of industrial utilization of formal concept selection methods was relatively low. Less than one out of four companies responded to use one or several of the formal methods included in the study: Pugh’s evaluation matrix, Rating matrices, or Analytic Hierarchy Process (AHP). Concept review meeting were reported as the most common approach for concept selection. However, a majority of the companies that did not utilize any formal method reported lacking effective and suitable methods for concept selection. The companies using formal methods were more satisfied. The first conclusion from the study is that there is a basis for a higher degree of utilization of formal concept selection methods in industry. Our second conclusion is that the existing formal concept selection methods do not entirely fulfill the needs of concept selection in an industry context. We propose that numerical concept selection methods should be further developed and extended to better support the decision-making practices of concept selection in industry. This type of concept selection is characterized by the participation of multiple decision makers through concept design reviews.

Bounded Prefix-Suffix Duplication: Language Theoretic and Algorithmic Results

2015 ◽  
Vol 26 (07) ◽  
pp. 933-952 ◽  
Author(s):  
Marius Dumitran ◽  
Javier Gil ◽  
Florin Manea ◽  
Victor Mitrana
Keyword(s):  
Efficient Algorithm ◽  
Regular Language ◽  
Regular Languages ◽  
Sufficient Condition ◽  
Membership Problem

We consider a restricted variant of the prefix-suffix duplication operation, called bounded prefix-suffix duplication. It consists in the iterative duplication of a length-bounded prefix or suffix of a given word. We give a sufficient condition for the closure of a class of languages under bounded prefix-suffix duplication. Consequently, we get that the class of regular languages is closed under bounded prefix-suffix duplication; furthermore, we propose an algorithm which decides whether a regular language is a finite k-prefix-suffix duplication language. An efficient algorithm solving the membership problem for the k-prefix-suffix duplication of a language is also presented. Finally, we define the k-prefix-suffix duplication distance between two words, extend it to languages and show how it can be computed for regular languages.

HYPER-MINIMIZATION IN O(n2)

2009 ◽  
Vol 20 (04) ◽  
pp. 735-746 ◽  
Author(s):  
ANDREW BADR
Keyword(s):  
Minimization Problem ◽  
Formal Languages ◽  
Regular Languages ◽  
Symmetric Difference ◽  
Finite Cover ◽  
Finite Set

Two formal languages are f-equivalent if their symmetric difference L1 Δ L2 is a finite set — that is, if they differ on only finitely many words. The study of f -equivalent languages, and particularly the DFAs that accept them, was recently introduced [3]. First, we restate the fundamental results in this new area of research. Second, we introduce our main result, which is a faster algorithm for the natural minimization problem: given a starting DFA D, find the smallest (by number of states) DFA D′ such that L(D) and L(D′) are f -equivalent. Finally, we suggest a technique that combines this hyper-minimization with the well-studied notion of a deterministic finite cover automaton [2, 4, 5], or DFCA, thereby extending the applicability of DFCAs from finite to infinite regular languages.

Sign in / Sign up

Export Citation Format

Share Document