Search

Signal temporal logic (STL) formulas have been widely used as a formal language to express complex robotic specifications, thanks to their rich expressiveness and explicit time semantics. Existing approaches for STL control synthesis suffer from limited scalability with respect to the task complexity and lack of robustness against the uncertainty, for example, external disturbances. In this paper, we study the online control synthesis problem for uncertain discrete-time systems subject to STL specifications. Different from existing techniques, we propose an approach based on STL, reachability analysis, and temporal logic trees. First, based on a real-time version of STL semantics, we develop the notion of tube-based temporal logic tree (tTLT) and its recursive (offline) construction algorithm. We show that the tTLT is an under-approximation of the STL formula, in the sense that a trajectory satisfying a tTLT also satisfies the corresponding STL formula. Then, an online control synthesis algorithm is designed using the constructed tTLT. It is shown that when the STL formula is robustly satisfiable and the initial state of the system belongs to the initial root node of the tTLT, it is guaranteed that the trajectory generated by the control synthesis algorithm satisfies the STL formula. We validate the effectiveness of the proposed approach by several simulation examples and further demonstrate its practical usability on a hardware experiment. These results show that our approach is able to handle complex STL formulas with long horizons and ensure the robustness against the disturbances, which is beyond the scope of the state-of-the-art STL control synthesis approaches. [ABSTRACT FROM AUTHOR]

We generalize the theory of linked partition ideals due to Andrews using finite automata in formal language theory and apply it to prove three Rogers-Ramanujan type identities for modulus 14 that were posed by Nandi through a vertex operator theoretic construction of the level 4 standard modules of the affine Lie algebra A(2) 2 . [ABSTRACT FROM AUTHOR]

Geometric problem solving (GPS) has always been a long-standing challenge in the fields of automated reasoning. Its problem representation and solution process embody rich symmetry. This paper is the second in a series of our works. Based on the Geometry Formalization Theory and the FormalGeo geometric formal system, we have developed the Formal Geometric Problem Solver (FGPS) in Python 3.10, which can serve as an interactive assistant or as an automated problem solver. FGPS is capable of executing geometric predicate logic and performing relational reasoning and algebraic computation, ultimately achieving readable, traceable, and verifiable automated solutions for geometric problems. We observed that symmetry phenomena exist at various levels within FGPS and utilized these symmetries to further refine the system's design. FGPS employs symbols to represent geometric shapes and transforms various geometric patterns into a set of symbolic operation rules. This maintains symmetry in basic transformations, shape constructions, and the application of theorems. Moreover, we also have annotated the formalgeo7k dataset, which contains 6981 geometry problems with detailed formal language descriptions and solutions. Experiments on formalgeo7k validate the correctness and utility of the FGPS. The forward search method with random strategy achieved a 39.71% problem-solving success rate. [ABSTRACT FROM AUTHOR]

Modeling and verification of the correct behavior of embedded real-time systems with strict timing constraints is a well-known and important problem. Failing to fulfill a deadline in system operation can have severe consequences in the practical case. This paper proposes an approach to formal modeling and schedulability analysis. A novel extension of Petri Nets named Constraint Time Petri Nets (C-TPN) is developed, which enables the modeling of a collection of interdependent real-time tasks whose execution is constrained by the use of priority and shared resources like processors and memory data. A C-TPN model is reduced to a network of Timed Automata in the context of the popular Uppaal toolbox. Both functional and, most importantly, temporal properties can be assessed by exhaustive model checking and/or statistical model checking based on simulations. This paper first describes and motivates the proposed C-TPN modeling language and its formal semantics. Then, a Uppaal translation is shown. Finally, three models of embedded real-time systems are considered, and their properties are thoroughly verified. [ABSTRACT FROM AUTHOR]

Specification languages for runtime verification are commonly rooted in formal languages, such as temporal logic, automata, or regular expressions. We argue that, for practical purposes, specification languages for monitoring should allow language features similar to those found in general purpose programming languages, in addition to providing specialized monitoring constructs. Using a realistic and large event-log, we compare two such programming-oriented monitoring language systems to a temporal logic-based monitoring system that was previously evaluated on the same log. The first programming-oriented language is a library in Scala developed for runtime verification. The other language is a scripting language, originally developed for fast static code analysis. We formulate the same reasonably complex properties as in the temporal logic case, using both methods, and compare the efficiency with which they can be checked against the large event log, and the ease with which the properties can be formulated. [ABSTRACT FROM AUTHOR]

Language is a unique ability of human beings. Although relatively simple for humans, the ability to understand human language is a highly complex task for machines. For a machine to learn a particular language, it must understand not only the words and rules used in a particular language, but also the context of sentences and the meaning that words take on in a particular context. In the experimental development we present in this paper, the goal was the development of the language model SRBerta—a language model designed to understand the formal language of Serbian legal documents. SRBerta is the first of its kind since it has been trained using Cyrillic legal texts contained within a dataset created specifically for this purpose. The main goal of SRBerta network development was to understand the formal language of Serbian legislation. The training process was carried out using minimal resources (single NVIDIA Quadro RTX 5000 GPU) and performed in two phases—base model training and fine-tuning. We will present the structure of the model, the structure of the training datasets, the training process, and the evaluation results. Further, we will explain the accuracy metric used in our case and demonstrate that SRBerta achieves a high level of accuracy for the task of masked language modeling in Serbian Cyrillic legal texts. Finally, SRBerta model and training datasets are publicly available for scientific and commercial purposes. [ABSTRACT FROM AUTHOR]

The Unified Modeling Language (UML) is a standard for modeling dynamic systems. UML behavioral state machines are used for modeling the dynamic behavior of object-oriented designs. The UML specification, maintained by the Object Management Group (OMG), is documented in natural language (in contrast to formal language). The inherent ambiguity of natural languages may introduce inconsistencies in the resulting statemachine model. Formalizing UML state machine specification aims at solving the ambiguity problem and at providing a uniform view to software designers and developers. Such a formalization also aims at providing a foundation for automatic verification of UML state machine models, which can help to find software design vulnerabilities at an early stage and reduce the development cost. We provide here a comprehensive survey of existing work from 1997 to 2021 related to formalizing UML state machine semantics for the purpose of conducting model checking at the design stage. [ABSTRACT FROM AUTHOR]

This paper advocates the use of compositional specifications based on formal languages as a means of modelling and analysing sophisticated collective behaviour in natural systems. With the use of appropriate linguistic constructs, models can be developed that are both compact and intuitive, and can be easily refined and extended in small steps. Automated workflows can be implemented on top of this methodology to provide quick feedback, enabling rapid design iterations. To support our argument, we present three examples from the natural world, focusing on flocks of birds and colonies of ants, which feature well-known examples of emergent behaviour in collective adaptive systems. We use an agent-based language to develop simple models that aim at capturing these collective phenomena, and discuss the specific language constructs that we use in the process. Then, we adapt an existing verification tool for the language to simulate our models, and show that our simulations do display emergent behaviour. [ABSTRACT FROM AUTHOR]

Depression is a severe mental health issue. The user‐generated content on social media (SM) is growing nowadays. Some computational approaches have been proposed for detecting depression based on users' SM data. However, because of the use of formal language, short range of words and misspellings in the SM data, depression detection (DD) is a challenging task. This paper proposes a novel deep learning (DL) technique for performing DD of the SM data with the help of the hybrid feature selection (FS) mechanism. Initially, two publicly available datasets containing user tweets are collected for implementing the proposed research model. Then the collected datasets are preprocessed for further processing. The preprocessing phase includes critical processes that contribute to creating a ready‐to‐use dataset for training and testing. After preprocessing, the preprocessed data is divided into prime and non‐prime words based on the dictionary approach. After that, the hybrid FS approach is implemented to select the most relevant features from the prime and non‐prime words for higher classification accuracy (AC). In the hybrid model, firstly Term Frequency Inverse Document Frequency integrated Modified Information Gain (TFIDF‐MIG) approach is proposed that assigns the score value of each prime and non‐prime word in the dataset. Secondly, optimal features are selected from the weighted features using the Improved Elephant Herding Algorithm (IEHA). Finally, the decided features from the hybrid model are fed into the DL model, namely attention included improved ReLU‐based Convolution Neural Network with Long Short‐Term Memory (AIRCNN‐LSTM) for DD. Experiments are performed on the collected datasets to assess the proposed model's performance efficiency. The results of the extensive experiments show that the presented work outperforms existing techniques regarding DD classification AC by locating the best solutions. At the same time, it reduces the number of features chosen. [ABSTRACT FROM AUTHOR]

According to the language-of-thought hypothesis, regular sequences are compressed in human memory using recursive loops akin to a mental program that predicts future items. We tested this theory by probing memory for 16-item sequences made of two sounds. We recorded brain activity with functional MRI and magneto-encephalography (MEG) while participants listened to a hierarchy of sequences of variable complexity, whose minimal description required transition probabilities, chunking, or nested structures. Occasional deviant sounds probed the participants' knowledge of the sequence. We predicted that task difficulty and brain activity would be proportional to the complexity derived from the minimal description length in our formal language. Furthermore, activity should increase with complexity for learned sequences, and decrease with complexity for deviants. These predictions were upheld in both fMRI and MEG, indicating that sequence predictions are highly dependent on sequence structure and become weaker and delayed as complexity increases. The proposed language recruited bilateral superior temporal, precentral, anterior intraparietal, and cerebellar cortices. These regions overlapped extensively with a localizer for mathematical calculation, and much less with spoken or written language processing. We propose that these areas collectively encode regular sequences as repetitions with variations and their recursive composition into nested structures. [ABSTRACT FROM AUTHOR]

Chan monks had a language problem. They needed to deal with at least four registers; the language of the street in their district, the Chan koine with its colloquialisms and argot, the guanhua or official language, and the elite formal language in Literary Sinitic that was packed with allusions. Zen monks in Japan had to deal with registers of Japanese, plus the Chan koine and the formal Literary Chinese. One response was philological, glosses on vocabulary that were likely to be misunderstood, such as dialect words and words that had changed meaning over time. Notably, most of these responses originated in or were connected to the greater Hangzhou region and its Wu language. After discussing whether there was a "standard" or common language used by elites throughout China, this article contends that the awareness of language differences between the "standard" or Mandarin Chinese and the Wu language by native Wu speakers contributed to the rise of Chan philology and then Zen philology. A few key examples of specialized Chan philological texts will be examined, but it should be kept in mind that examples of Chan philology may be embedded in other Chan works. [ABSTRACT FROM AUTHOR]

We contribute to the refined understanding of language-logic-algebra interplay in a recent algebraic framework over countable words. Algebraic characterizations of the one variable fragment of FO as well as the boolean closure of the existential fragment of FO are established. We develop a seamless integration of the block product operation in the countable setting, and generalize well-known decompositional characterizations of FO and its two variable fragment. We propose an extension of FO admitting infinitary quantifiers to reason about inherent infinitary properties of countable words, and obtain a natural hierarchical block-product based characterization of this extension. Properties expressible in this extension can be simultaneously expressed in the classical logical systems such as WMSO and FO[cut]. We also rule out the possibility of a finite-basis for a block-product based characterization of these logical systems. Finally, we report algebraic characterizations of one variable fragments of the hierarchies of the new extension. [ABSTRACT FROM AUTHOR]

Recently, the emerging technologies have been constantly shaping the education domain, especially the use of artificial intelligence (AI) for language learning, which has attracted significant attention. Many of the AI tools are being used for learning foreign languages, in both formal and informal ways. There are many studies that have explored the potential of the recent technology "ChatGPT" for education and learning languages, but none of the existing studies have conducted any exploratory study for assessing the usability of ChatGPT. This paper conducts an assessment for usability of ChatGPT for formal English language learning. The study uses a standard questionnaire-based approach to ask participants about their feedback for usefulness and effectiveness of ChatGPT. The participants were asked for their feedback after performing series of tasks related to formal English language learning with ChatGPT. A variety of student participants were selected for this study with diverse English language proficiency levels, education levels, and nationalities. The quantitative analysis of the participant responses shed light on their experience with regards to the usability of ChatGPT for performing different English language learning tasks such as conversation, writing, grammar, and vocabulary. The findings from this study are quite promising and indicate that ChatGPT is an effective tool to be used for formal English language learning. Overall, this study contributes to the fast-growing research domain on using emerging technologies for formal English language learning by conducting in-depth assessment of usability for ChatGPT in formal English language learning. [ABSTRACT FROM AUTHOR]

One-dimensional (string) formal languages and their learning have been studied in considerable depth. However, the knowledge of their two-dimensional (picture) counterpart, which retains similar importance, is lacking. We investigate the problem of learning formal two-dimensional picture languages by applying learning methods for one-dimensional (string) languages. We formalize the transcription process from a two-dimensional input picture into a string and propose a few adaptations to it. These proposals are then tested in a series of experiments, and their outcomes are compared. Finally, these methods are applied to a practical problem and an automaton for recognizing a part of the MNIST dataset is learned. The obtained results show improvements in the topic and the potential to use the learning of automata in fitting problems. [ABSTRACT FROM AUTHOR]

This paper presents a technique, named STLCG, to compute the quantitative semantics of Signal Temporal Logic (STL) formulas using computation graphs. STLCG provides a platform which enables the incorporation of logical specifications into robotics problems that benefit from gradient-based solutions. Specifically, STL is a powerful and expressive formal language that can specify spatial and temporal properties of signals generated by both continuous and hybrid systems. The quantitative semantics of STL provide a robustness metric, that is, how much a signal satisfies or violates an STL specification. In this work, we devise a systematic methodology for translating STL robustness formulas into computation graphs. With this representation, and by leveraging off-the-shelf automatic differentiation tools, we are able to efficiently backpropagate through STL robustness formulas and hence enable a natural and easy-to-use integration of STL specifications with many gradient-based approaches used in robotics. Through a number of examples stemming from various robotics applications, we demonstrate that STLCG is versatile, computationally efficient, and capable of incorporating human-domain knowledge into the problem formulation. [ABSTRACT FROM AUTHOR]

In this work, computer-assisted writing techniques for linear expressions of the structure of polycyclic molecules, branched molecules and clusters, based on formal languages, are tested. The techniques used only require the ability to process written texts, even just using a text editor, and one of the many available molecular drawing/optimization programs that accept input in the form of a SMILES string. A few specific syntactic operators acting on strings are characterized in terms of their effect on the corresponding structure, and although they are simply examples, they are already capable of producing non-trivial structures. The aim of this work is to encourage experiments that may lead to potentially interesting molecular schemata, in view of their symmetry and stereochemistry, as revealed by optimization, and to develop insight into the connection between formal expressions and structures. Given the simplicity and availability of the required tools, it can also be useful for education. [ABSTRACT FROM AUTHOR]

dition of standardizing word meanings in Estonian language planning. The tradition of the Estonian language planning to standardize the meanings of general language through the formal Dictionary of Standard Estonian (DSE) has long influenced society’s understanding of how (Estonian) language works. Since the 1980s, instead of standardizing the meanings, the language planning has been more “lenient”, considering certain meanings inappropriate for the standard language and making recommendations on them (e.g. in the DSE 1999–2018). In this article, we will give an overview of the history of the standardization of word meanings in the Estonian language planning since the second half of the 19th century, analyzing the most important publications related to it. We draw generalizations and conclusions about the standardization of meanings based on our earlier research on word meanings: with the deepening of usagebased linguistics and corpus linguistics in Estonian linguistics, the understanding has been reached in language planning that meanings do not remain fixed in the dictionary: the (new) meaning’s survival in use depends on internal and external factors, not on the formal DSE. [ABSTRACT FROM AUTHOR]

Word algebra problems are among challenging AI tasks as they combine natural language understanding with a formal equation system. Traditional approaches to the problem work with equation templates and frame the task as a template selection and number assignment to the selected template. The recent deep learning-based solutions exploit contextual language models like BERT and encode the natural language text to decode the corresponding equation system. The proposed approach is similar to the template-based methods as it works with a template and fills in the number slots. Nevertheless, it has contextual understanding because it adopts a question generation and answering pipeline to create tuples of numbers, to finally perform the number assignment task by custom sets of rules. The inspiring idea is that by asking the right questions and answering them using a state-of-the-art language model-based system, one can learn the correct values for the number slots in an equation system. The empirical results show that the proposed approach outperforms the other methods significantly on the word algebra benchmark dataset alg514 and performs the second best on the AI2 corpus for arithmetic word problems. It also has superior performance on the challenging SVAMP dataset. Though it is a rule-based system, simple rule sets and relatively slight differences between rules for different templates indicate that it is highly probable to develop a system that can learn the patterns for the collection of all possible templates, and produce the correct equations for an example instance. [ABSTRACT FROM AUTHOR]

This paper presents the HybridSynchAADL modeling language and formal analysis tool for virtually synchronous cyber-physical systems with complex control programs, continuous behaviors, and bounded clock skews, network delays, and execution times. We leverage the Hybrid PALS methodology, so that it is sufficient to model and verify the much simpler underlying synchronous designs. We define the HybridSynchAADL language as a sublanguage of the avionics modeling standard AADL for modeling such synchronous designs in AADL. We define the formal semantics of HybridSynchAADL using Maude with SMT solving, which allows us to represent advanced control programs and communication features in Maude, while capturing timing uncertainties and continuous behaviors symbolically with SMT solving. We have developed new general methods for optimizing the performance of such symbolic rewriting, which makes the analysis of HybridSynchAADL models feasible. We have integrated the formal modeling and analysis of HybridSynchAADL models into the OSATE tool environment for AADL. Finally, we demonstrate the effectiveness of the Hybrid PALS methodology and HybridSynchAADL on a number of applications, including autonomous drones that collaborate to achieve common goals, and compare the performance of our tool with other state-of-the-art formal tools for hybrid systems. [ABSTRACT FROM AUTHOR]

Summary: In this work we elaborate on the idea of a formal theory for a limited but important part of structural chemistry, that described by Lewis' methods and VSEPR (Valence Shell Electron Pair Repulsion). For this purpose, recursive functions and propositional functions are defined, that apply to formal expressions of the structure, based on a finite set of symbols. This approach allows for the expression of numerous questions of chemical interest. The formalization of basic structural chemistry based on Lewis/VSEPR method is potentially useful for the automation of the related procedures, but possibly also of some use as complementary material in teaching and as a heuristic tool in structural chemistry. [ABSTRACT FROM AUTHOR]

In the present paper, we aim to develop a formal quantum logic theory of the interplay between conscious and unconscious processes of the human mind, a goal that has already been envisaged in quantum cognition; in doing so, we will show how the interplay between formal language and metalanguage allows for characterizing pure quantum states as infinite singletons: in the case of the spin observable, we obtain an equation defining a modality that is then re-interpreted as an abstract projection operator. By including a temporal parameter in the equations and by defining a modal negative operator, we derive an intuitionistic-like negation, for which the non-contradiction law is seen as an equivalent of the quantum uncertainty. Building on the psychoanalytic theory of Bi-Logic by Matte Blanco, we use modalities in interpreting the emergence of conscious representations from an unconscious one, and we demonstrate that this description fits well with Freud's view of the role of negation in mental processes. Psychoanalysis, where affect plays a prominent role in shaping not only conscious, but also unconscious representations, is therefore seen as a suitable model to expand the domain of quantum cognition to the broader field of affective quantum cognition. [ABSTRACT FROM AUTHOR]

Let Σ + be the set of all finite words over a finite alphabet Σ. A word u is called a strict prefix of a word v, if u is a prefix of v and there is no other way to show that u is a subword of v. A language L ⊆ Σ + is said to be prefix-strict, if for any u , v ∈ L , u is a subword of v always implies that u is a strict prefix of v. Denote the class of all prefix-strict languages in Σ + by P (Σ +) . This paper characterizes P (Σ +) as a universe of a model of the free object for the ai-semiring variety satisfying the additional identities x + y x ≈ x and x + y x z ≈ x . Furthermore, the analogous results for so-called suffix-strict languages and infix-strict languages are introduced. [ABSTRACT FROM AUTHOR]

This review presents various perspectives on converting user keywords into a formal query. Without understanding the dataset's underlying structure, how can a user input a text-based query and then convert this text into semantic protocol and resource description framework query language (SPARQL) that deals with the resource description framework (RDF) knowledge base? The user may not know the structure and syntax of SPARQL, a formal query language and a sophisticated tool for the semantic web (SEW) and its vast and growing collection of interconnected open data repositories. As a result, this study examines various strategies for turning natural language into formal queries, their workings, and their results. In an Internet search engine from a single query, such as on Google, numerous matching documents are returned, with several related to the inquiry while others are not. Since a considerable percentage of the information retrieved is likely unrelated, sophisticated information retrieval systems based on SEW technologies, such as RDF and web ontology language (OWL), can help end users organize vast amounts of data to address this issue. This study reviews this research field and discusses two different approaches to show how users with no knowledge of the syntax of semantic web technologies deal with queries. [ABSTRACT FROM AUTHOR]

Polymers are widely studied materials with diverse properties and applications determined by molecular structures. It is essential to represent these structures clearly and explore the full space of achievable chemical designs. However, existing approaches cannot offer comprehensive design models for polymers because of their inherent scale and structural complexity. Here, a parametric, context‐sensitive grammar designed specifically for polymers (PolyGrammar) is proposed. Using the symbolic hypergraph representation and 14 simple production rules, PolyGrammar can represent and generate all valid polyurethane structures. An algorithm is presented to translate any polyurethane structure from the popular Simplified Molecular‐Input Line‐entry System (SMILES) string format into the PolyGrammar representation. The representative power of PolyGrammar is tested by translating a dataset of over 600 polyurethane samples collected from the literature. Furthermore, it is shown that PolyGrammar can be easily extended to other copolymers and homopolymers. By offering a complete, explicit representation scheme and an explainable generative model with validity guarantees, PolyGrammar takes an essential step toward a more comprehensive and practical system for polymer discovery and exploration. As the first bridge between formal languages and chemistry, PolyGrammar also serves as a critical blueprint to inform the design of similar grammars for other chemistries, including organic and inorganic molecules. [ABSTRACT FROM AUTHOR]

Commutative properties in formal languages pose problems at the frontier of computer science, computational linguistics and computational group theory. A prominent problem of this kind is the position of the language O n , the language that contains the same number of letters a i and a ¯ i with 1 ⩽ i ⩽ n , in the known classes of formal languages. It has recently been shown that O n is a Multiple Context-Free Language (MCFL). However the more precise conjecture of Nederhof that O n is an MCFL of dimension n was left open. We prove this conjecture using tools from algebraic topology. On our way, we prove a variant of the necklace splitting theorem. [ABSTRACT FROM AUTHOR]

We consider the computability and complexity of decision questions for Probabilistic Finite Automata (PFA) with sub-exponential ambiguity. We show that the emptiness problem for strict and non-strict cut-points of polynomially ambiguous commutative PFA remains undecidable, implying that the problem is undecidable when inputs are from a letter monotonic language. We show that the problem remains undecidable over a binary input alphabet when the input word is over a bounded language, in the noncommutative case. In doing so, we introduce a new technique based upon the Turakainen construction of a PFA from a Weighted Finite Automaton which can be used to generate PFA of lower dimensions and of sub-exponential ambiguity. We also study freeness/injectivity problems for polynomially ambiguous PFA and study the border of decidability and tractability for various cases. [ABSTRACT FROM AUTHOR]

The regular intersection emptiness problem for a decision problem P ( int Reg (P)) is to decide whether a potentially infinite regular set of encoded P-instances contains a positive one. Since int Reg (P) is decidable for some NP-complete problems and undecidable for others, its investigation provides insights in the nature of NP-complete problems. Moreover, the decidability of the int Reg -problem is usually achieved by exploiting the regularity of the set of instances; thus, it also establishes a connection to formal language and automata theory. We consider the int Reg -problem for the well-known NP-complete problem Integer Linear Programming (ILP). It is shown that any DFA that describes a set of ILP-instances (in a natural encoding) can be reduced to a finite core of instances that contains a positive one if and only if the original set of instances did. This result yields the decidability of int Reg (ILP). [ABSTRACT FROM AUTHOR]

Traditionally, graph algorithms get a single graph as input, and then they should decide if this graph satisfies a certain property Φ . What happens if this question is modified in a way that we get a possibly infinite family of graphs as an input, and the question is if there is a graph satisfying Φ in the family? We approach this question by using formal languages for specifying families of graphs, in particular by regular sets of words. We show that certain graph properties can be decided by studying the syntactic monoid of the specification language L if a certain torsion condition is satisfied. This condition holds trivially if L is regular. More specifically, we use a natural binary encoding of finite graphs over a binary alphabet Σ , and we define a regular set G ⊆ Σ ∗ such that every nonempty word w ∈ G defines a finite and nonempty graph. Also, graph properties can then be syntactically defined as languages over Σ . Then, we ask whether the automaton A specifies some graph satisfying a certain property Φ . Our structural results show that we can answer this question for all "typical" graph properties. In order to show our results, we split L into a finite union of subsets and every subset of this union defines in a natural way a single finite graph F where some edges and vertices are marked. The marked graph in turn defines an infinite graph F ∞ and therefore the family of finite subgraphs of F ∞ where F appears as an induced subgraph. This yields a geometric description of all graphs specified by L based on splitting L into finitely many pieces; then using the notion of graph retraction, we obtain an easily understandable description of the graphs in each piece. [ABSTRACT FROM AUTHOR]

Prior research indicates that humans adapt their language depending on context. This linguistic sensitivity has been suggested to indicate a natural pedagogy shared by all humans. This sensitivity has, however, only been demonstrated with English‐speaking samples thus far. In two studies, we followed the experimental procedure of the original study to replicate their findings with German‐speaking samples. With Study 2 conducted in the diglossic environment of the German‐speaking part of Switzerland, we were additionally able to provide a first test for whether this sensitivity is restricted to the language spoken in formal educational settings or occurs also in everyday language. Across both studies, we found a more frequent use of generic utterances in the pedagogical context than in the nonpedagogical context, both in Germany (Study 1) and in Switzerland (Study 2). These results and the strong effect sizes provide clear support for a natural pedagogy. [ABSTRACT FROM AUTHOR]

Typically recognized as informal, inaccurate and haphazard, slang, a form of unstructured language that violates the standard rules of English language (Geertsema, Hyman, & Van Deventer, 2011) is gradually seeping into everyday language use. The present study investigates the impact of slangs in the Pakistani context, where students use English as a second language and the main language for their tertiary education. The study is informed by the works of Wardaugh, (2011) centring on the connection between language variation and society. The quantitative study uses an explanatory research design with a purposively selected sample of 70 English major undergraduate students from a government university. The data was collected from students’ survey questionnaire which was then analysed using descriptive statistics. The findings reveal that the formal language use is impacted due to constant variation in language caused by the society as language and society are interdependent. [ABSTRACT FROM AUTHOR]

Mathematics employs a formal language where symbols, verbs, and nouns serve to express terms, concepts, and rules that concatenate to definitions, problem-solving procedures, and proofs. Taken together these constitute the expository language of mathematics found in journals, textbooks, and demonstrations. As the object of these mathematical communications is to inform and perhaps inspire, there are epistemological and ethical considerations that deserve examination. For in keeping with the commitment to an aesthetic of concision promulgated by tradition, the formal presentation language and style of mathematics, while valuable in furthering the body of knowledge, provides only the conclusion of an inquiry, completely excluding the language of investigation that informed the many steps of decision making involved in the process, so that little if any insight into the creative process is made available. Here we explore this problem of communication in the context of mathematics presented to students early in their education as well as at university level. The argument is made that the language of investigation -- the heuristic actions instrumental for their formulation -- ought to accompany the language of formal demonstration so as to provide a communication that is in the best interests of all students and members of the mathematics profession. [ABSTRACT FROM AUTHOR]

• Examine young bilinguals with distant languages (L1: Chinese and L2: English). • The early literacy transfer between L1 and L2 in an L1-dominant environment. • Use functional near-infrared spectroscopy to study transfer on phoneme awareness. • The L2 transfer on the left dorsal neural pathways with phonological processing. • The L1 transfer on the right frontal regions with increased cognitive load. The growing trend of bilingual education between Chinese and English has contributed to a rise in the number of early bilingual children, who were exposed to L2 prior to formal language instruction of L1. The L2-L1 transfer effect in an L1-dominant environment has been well established. However, the threshold of L2 proficiency at which such transfer manifests remains unclear. This study investigated the behavioral and neural processes involved when manipulating phonemes in an auditory phonological task to uncover the transfer effect in young bilingual children. Sixty-two first graders from elementary schools in Taiwan were recruited in this study (29 Chinese monolinguals, 33 Chinese-English bilinguals). The brain activity was measured using fNIRS (functional near-infrared spectroscopy). Bilingual children showed right lateralization to process Chinese and left lateralization to process English, which supports more on the accommodation effect within the framework of the assimilation-accommodation hypothesis. Also, compared to monolinguals, bilingual children showed more bilateral frontal activation in Chinese, potentially reflecting a mixed influence from L2-L1 transfer effects and increased cognitive load of bilingual exposure. These results elucidate the developmental adjustments in the neural substrates associated with early bilingual exposure in phonological processing, offering valuable insights into the bilingual learning process. [ABSTRACT FROM AUTHOR]

The last chapter (Chapter 8) presents an interesting discussion of future steps from a variety of perspectives, connecting finite-state methods to current trends in the field. The first half of the book serves as an introduction to core concepts in formal language and automata theory (Chapter 1), the basic design principles of the Python library used through the book (Chapter 2), and a variety of finite-state algorithms (Chapters 3 and 4). However, the chapter lays down these theoretical notions clearly, and its stands as an intriguing starting point for any reader interested in learning more about the mathematics of monoids and formal languages. [Extracted from the article]

Coverings of undirected graphs are used in distributed computing, and unfoldings of directed graphs in semantics of programs. We study these two notions from a graph theoretical point of view so as to highlight their similarities, as they are both defined in terms of surjective graph homomorphisms. In particular, universal coverings and complete unfoldings are infinite trees that are regular if the initial graphs are finite. Regularity means that a tree has finitely many subtrees up to isomorphism. Two important theorems have been established by Leighton and Norris for coverings of finite graphs. We prove similar results for unfoldings of finite directed graphs. Moreover, we generalize coverings and similarly, unfoldings to graphs and digraphs equipped with finite or infinite weights attached to edges of the covered or unfolded graphs. This generalization yields a canonical "factorization" of the universal covering of any finite graph, that (provably) does not exist without using weights. Introducing ω as an infinite weight provides us with finite descriptions of regular trees having nodes of countably infinite degree. Regular trees (trees having finitely many subtrees up to isomorphism) play an important role in the extension of Formal Language Theory to infinite structures described in finitary ways. Our weighted graphs offer effective descriptions of the above mentioned regular trees and yield decidability results. We also generalize to weighted graphs and their coverings a classical factorization theorem of their characteristic polynomials. [ABSTRACT FROM AUTHOR]

The replacement of the simple form verbal future by a periphrastic form consisting of auxiliary ir in the present followed by the infinitive of the main verb fits into a general tendency of the Romance languages to substitute synthetic verbal forms for analytical ones that go back to their Latin origins. This change is very advanced in Brazil, being that simple future is already almost absent from Brazilian vernacular speech, although its use remains in writing and in the more formal uses of the language. However, it is observed that the use of the present indicative for future expression remains constant. This variant corresponds to one fifth of the verbal forms that express futurity. Based on a quantitative variationist analysis, this article will seek to characterize this use as a structural niche in the process of variation and change. It is determined by very precise structural restrictions, but is not affected by extralinguistic factors, which would explain its maintenance. [ABSTRACT FROM AUTHOR]

The present paper describes an alternative algorithm for the removal of erasing rules fromE0S grammars. As opposed to the standard way of eliminating erasing rules in most E0S-like grammars, such as context-free grammars, this method requires no predetermination of symbols that derive the empty string. The proposed algorithm is formally verified. In the conclusion of the paper, the applicability of the algorithm to E0S grammars that work in a semi-parallel way is demonstrated. Furthermore, two open problems are formulated. [ABSTRACT FROM AUTHOR]

We prove lower bounds on the length of regular expressions for finite languages by methods from arithmetic circuit complexity. First, we show a reduction: the length of a regular expression for a language L ⊆ { 0 , 1 } n is bounded from below by the minimum size of a monotone arithmetic formula computing a polynomial that has L as its set of exponent vectors. This result yields lower bounds for the language of all words with exactly k ones and n − k zeros and for the language of all Dyck words of length 2 n. Second, we adapt a lower bound method for multilinear arithmetic formulas by so-called log-product polynomials to regular expressions. With this method we show almost tight lower bounds for the language of all n -bit binary numbers that are divisible by a given odd integer p and for the language of all permutations of { 1 , ... , n }. [ABSTRACT FROM AUTHOR]

Using techniques derived from the syntactic methods for visual pattern recognition is not new and was much explored in the area called syntactical or structural pattern recognition. Syntactic methods have been useful because they are intuitively simple to understand and have transparent, interpretable, and elegant representations. Their capacity to represent patterns in a semantic, hierarchical, compositional, spatial, and temporal way have made them very popular in the research community. In this article, we try to give an overview of how syntactic methods have been employed for computer vision tasks. We conduct a systematic literature review to survey the most relevant studies that use syntactic methods for pattern recognition tasks in images and videos. Our search returned 597 papers, of which 71 papers were selected for analysis. The results indicated that in most of the studies surveyed, the syntactic methods were used as a high-level structure that makes the hierarchical or semantic relationship among objects or actions to perform the most diverse tasks. [ABSTRACT FROM AUTHOR]

Much of the confusion about the proper regulation of smart contracts stems from the fact that both code and law are expressed in language. Natural (human) and formal (computer) languages are profoundly different, however. Natural language in the form of a true legal contract expresses human meaning and expectation. Code simply acts, and when code acts contrary to the understanding of the parties to a contract, courts must have a theoretical and legal basis in order to intervene—which this Article provides. Present scholarship on the governance of smart contracts centers on logistical problems relating to the effects of automation on operation and execution, most notably problems of inflexibility and lack of enforcement discretion. However, automatic execution is nothing new in contract law. Rather, it is the legal interface between contract law and code that must catch and hold our attention. We focus on the point where the ‘natural language’ of contract law crosses over into the ‘formal language’ of computer code. Natural language contract terms are made accessible to a human and receive some sort of confirmation to establish the contractual magic, a set of bespoke legal rules between two parties encapsulated in some document or through behavior that makes the intention of the parties unmistakable. The formal language program portion of a smart contract executes, sometimes in accordance with these expectations, sometimes not. This Article asserts that human expectations determine the legal obligations of a contract, and that code merely executes it. It then explores the legal bases and ramifications of this human-centered law of smart contracting. [ABSTRACT FROM AUTHOR]

The study of the splicing system swiftly grew after Tom Head investigated the biochemical process modelling involving the DNA in 1987. The process of the splicing system consists of a cut and paste of the DNA molecules. Splicing language produced by the splicing system can be classified into inert, transient, and limit language. Previously, second-order limit language was described as a new set of language from the previous splicing language. In this research, we would like to extend the study to n-th order limit language by investigating the effect of the number of rules involved in the splicing system. Following from here, its properties are explored using the formal language theory. [ABSTRACT FROM AUTHOR]

A major goal of linguistics and cognitive science is to understand what class of learning systems can acquire natural language. Until recently, the computational requirements of language have been used to argue that learning is impossible without a highly constrained hypothesis space. Here, we describe a learning system that is maximally unconstrained, operating over the space of all computations, and is able to acquire many of the key structures present in natural language from positive evidence alone. We demonstrate this by providing the same learning model with data from 74 distinct formal languages which have been argued to capture key features of language, have been studied in experimental work, or come from an interesting complexity class. The model is able to successfully induce the latent system generating the observed strings from small amounts of evidence in almost all cases, including for regular (e.g., an, (ab)n, and {a,b}+, context-free (e.g., anbn, anbn+m, and xxR), and context-sensitive (e.g., anbncn, anbmcndm, and xx) languages, as well as for many languages studied in learning experiments. These results show that relatively small amounts of positive evidence can support learning of rich classes of generative computations over structures. The model provides an idealized learning setup upon which additional cognitive constraints and biases can be formalized. [ABSTRACT FROM AUTHOR]

Previous research has hypothesized that human sequential processing may be dependent upon hearing experience (the "auditory scaffolding hypothesis"), predicting that sequential rule learning abilities should be hindered by congenital deafness. To test this hypothesis, we compared deaf signer and hearing individuals' ability to acquire rules of different computational complexity in a visual artificial grammar learning task using sequential stimuli. As a group, deaf participants succeeded at all levels of the task; Bayesian analysis indicates that they successfully acquired each of several target grammars at ascending levels of the formal language hierarchy. Overall, these results do not support the auditory scaffolding hypothesis. However, age‐ and education‐matched hearing participants did outperform deaf participants in two out of three tested grammars. We suggest that this difference may be related to verbal recoding strategies in the two groups. Any verbal recoding strategies used by the deaf signers would be less effective because they would have to use the same visual channel required for the experimental task. [ABSTRACT FROM AUTHOR]

The present study is dedicated to the description of one of the areas in which an asymmetry in the linguistic choices available to Cape Verdeans is easily noticed, that is, the national education system. Firstly, we will trace the socio-historical context of the use of Portuguese and Cape Verdean in higher education, including some information about basic and secondary education. In the second part, we will present the results of the research carried out in 2016/2017 on the island of São Vicente, in Cape Verde, referring to the opinions of university students and the teaching staff regarding, for instance, the mandatory use of the Portuguese language in the school environment or the scarce presence of the national language in the formal higher education. For the purposes of this study, we chose 60 interviews: 37 with students from the University of Mindelo (UM), 15 with students from the University of Cape Verde (Uni-CV) and 8 with university professors, specialists in different scientific areas (Uni- CV, UM). The methodology applied for its description will be qualitative, with summarizing quantitative elements. The final observations, due to the small number of participants, cannot be considered as representative of the opinion of the entire population of São Vicente island, but they can, however, constitute a starting point for more comprehensive studies. [ABSTRACT FROM AUTHOR]

A current trend in research on multi-agent control systems is to consider high-level task specifications that go beyond traditional control objectives and take into account the heterogeneity of each agent in the system, i.e., the different capabilities of the agents in terms of actuation, sensing, communication and computation. This article provides an overview of our work on the problem of control of heterogeneous multi-agent systems under both spatial and temporal constraints as well as our perspective on the challenges and open problems associated with the consideration of such spatiotemporal constraints. Initially, we review a set of control strategies introduced by the authors addressing the satisfaction of cooperative tasks such as formation control as well as individual objectives such as reference tracking. The satisfaction of those objectives is ensured using prescribed performance control. Building upon these approaches we then review recent results on control under high-level spatiotemporal objectives expressed in Signal Temporal Logic, a formal language that allows to express complex spatial tasks that must be satisfied within pre-defined deadlines. Theoretical results considering multi-agent systems with various capabilities under spatiotemporal constraints are presented. [ABSTRACT FROM AUTHOR]

Novel computing paradigms, e.g., the Cloud, introduce new requirements with regard to access control such as utilization of historical information and continuity of decision. However, these concepts may introduce an additional level of complexity to the underpinning model, rendering its definition and verification a cumbersome and prone to errors process. Using a formal language to specify a model and formally verify it may lead to a rigorous definition of the interactions amongst its components, and the provision of formal guarantees for its correctness. In this paper, we consider a case study where we specify a formal model in TLA + for both a policy-neutral and policy-specific UseCON usage control model. Through that, we anticipate to shed light in the analysis and verification of usage control models and policies by sharing our experience when using TLA + specific tools. [ABSTRACT FROM AUTHOR]

Thomas Erlebach did his diploma project with Klaus-Jörn in München; Thomas is now a full professor at the University of Durham, UK. This special issue of I Acta Informatica i is dedicated to Professor Dr. Klaus-Jörn Lange on the occasion of his 70th birthday on the 9th of July, 2022. Yet, Klaus-Jörn and Volker knew each other already from their studies in Hamburg; Volker is currently a full professor in Stuttgart. [Extracted from the article]