Search

Assessments constitute a fundamental and inevitable component of any educational journey. Manual effort required for the evaluation of these assessments is very high. Automation of the evaluation process and grading helps in making the review process more efficient, objective, and scalable, thereby reducing the workload of human reviewers. Automating the grading process for multiple-choice and short-answer assessments is relatively straightforward, but it poses significant challenges when applied to the evaluation of formal languages, particularly in the context of mathematical assessments. In this paper a model that automatically evaluates and grades the Quadratic Equation problems is presented. The study is conducted using a manually curated dataset comprising 1200 solutions to various quadratic equation problems. Embeddings of the quadratic solutions are generated using Google's T5 Model. These embeddings are then used to train different traditional and ensembled machine learning models along with complex Deep learning models like LSTM and Bi LSTM. An in-depth analysis of the fine-tuned T5 model's performance, evaluating its effectiveness in comparison with the pretrained T5 model in automatic grading of quadratic equation problems has been explored. Fine-tuning significantly contributes to the reduction of error by 70% and a noticeable increase in the R2 value to 97%. [ABSTRACT FROM AUTHOR]

Requirements Engineering (RE) activity is often initiated with vaguely specified software requirements. The ambiguities must be overcome to the extent possible when the requirements are specified. Both functional (FRs) and non-functional (NFRs) requirements should be correctly and unambiguously specified. Users communicate about the NFRs in informal discussions. Requirements engineers use formal or semi-formal language notations to manually convey the NFRs. A laborious and ineffective manual approach, however, is unable to identify all likely NFRs and resolve ambiguities in those NFRs. This paper discusses an approach that attempts to overcome ambiguities from natural language requirements, recognize NFRs, and generate NFR specification through the extended Unified Modelling Language (UML) viz. use-case diagram. The empirical evaluation of the proposed approach on the PROMISE dataset achieves an average result of 79.76% recall, 90.05% precision, and 84.59% F-measure. The proposed approach allows the requirements analyst to semi-automatically recognize NFRs and visualize them using an extended use-case diagram at an early stage of RE. [ABSTRACT FROM AUTHOR]

Most modern regular expression matching libraries (one of the rare exceptions being Google's RE2) allow backreferences, operations which bind a substring to a variable, allowing it to be matched again verbatim. However, both real-world implementations and definitions in the literature use different syntactic restrictions and have differences in the semantics of the matching of backreferences. Our aim is to compare these various flavors by considering the classes of formal languages that each can describe, establishing, as a result, a hierarchy of language classes. Beyond the hierarchy itself, some complexity results are given, and as part of the effort on comparing language classes new pumping lemmas are established, old classes are extended to new ones, and several incidental results on the nature of these language classes are given. [ABSTRACT FROM AUTHOR]

We study a sound verification method for parametric component-based systems. The method uses a resource logic, a new formal specification language for distributed systems consisting of a finite yet unbounded number of components. The logic allows the description of architecture configurations coordinating instances of a finite number of types of components, by means of inductive definitions similar to the ones used to describe algebraic data types or recursive data structures. For parametric systems specified in this logic, we show that decision problems such as reaching deadlock or violating critical section are undecidable, in general. Despite this negative result, we provide for these decision problems practical semi-algorithms relying on the automatic synthesis of structural invariants allowing the proof of general safety properties. The invariants are defined using the WS κ S fragment of the monadic second order logic, known to be decidable by a classical automata-logic connection, thus reducing a verification problem to checking satisfiability of a WS κ S formula. • We introduce a logic-based language for describing sets of configurations of parameterized distributed systems. • The language uses predicate symbols to hierarchically decompose the system architecture into specific patterns. • We address a parametric safety problem i.e., checking that reachable configurations stay clear of error configurations. • We show that deadlock freedom and critical section violation problems are undecidable, even for simple architectures. • We develop a verification method that synthesizes parametric invariants described using a decidable fragment of MSO. [ABSTRACT FROM AUTHOR]

In the vein of a renewed interest in diagrammatic reasoning, this paper challenges an opposition between logic diagrams and formal languages that has traditionally been the common view in philosophy of logic and linguistics. We examine, from a philosophical point of view, what we call five dogmas of logic diagrams. These are as follows: (1) diagrams are non-linguistic; (2) diagrams are visual representations; (3) diagrams are iconic, and not symbolic; (4) diagrams are non-linear; (5) diagrams are heterogenous, and not homogenous. Using historical examples, we argue that none of these dogmas is an adequate criterion to distinguish logic diagrams from formal languages. Instead, we advocate that there is a common core between linguistic and diagrammatic representation and reasoning. • We critically examine, from a philosophical point of view, five dogmas in current research on logic diagrams that have been proposed as criteria to establish an opposition between formal language and logic diagrams. • The dogmas we consider are: (1) diagrams are non-linguistic ; (2) diagrams are visual representations; (3) diagrams are iconic , and not symbolic ; (4) diagrams are non-linear; (5) diagrams are heterogenous , and not homogenous. • We present historical examples which are not met by these criteria. • We provide a positive outlook by arguing that there is a common core between linguistic and diagrammatic representation and reasoning, which can be called 'invariance'. [ABSTRACT FROM AUTHOR]

In a multi-agent dynamic common-policy decision-making environment, by asking questions, an agent can generate an agreement on dynamically changing (on the fly, during the decision-making process) the common policy shared by the agents, and therefore, it can change the current list of possible options from which the decision is made. Important efforts were previously undertaken to define the Logic of Preferential Choice (LPC) as a model in which the so-called Condorcet Driver Paradox (CDP) and, more general, other apparently paradoxical decisions are legal syntaxes and valid formulas. On the contrary, we prove here that CDP can be easily dismounted in many formal languages – such as English, Arithmetic, SQL, Binary Logic, and Probabilities) - languages that are not only appropriate for modeling the process of question asking, but they are also proved as productive perspectives in decision-making, much popular in the community, much simpler and much largely accepted than the Logic of Preferential Choice. [ABSTRACT FROM AUTHOR]

In formal language theory, if a grammar consists of rules of the type (r , F r) , where r is a context-free rule and F r is an associated finite set of strings called the forbidding set, such that r can be applied to a string only if none of the strings in F r is present in the string, then the grammar is said to be a generalized forbidding (GF) grammar. There are four main parameters that describe the size of a GF grammar, namely, (1) d , the maximum length of strings in the forbidding sets, (2) i , the maximum cardinality of the forbidding sets, (3) n , the number of nonterminals used in the grammar, and (4) c , the number of rules with nonempty forbidding set. The family of languages described by a GF grammar of size (at most) (d , i , n , c) is denoted by GF (d , i , n , c). We study for what sizes of GF grammars one can obtain the computational power of Turing machines. We specifically show this result for sizes (2, 6, 8, 6), (2, 5, 9, 7), (2, 4, 7, 8) and (2, 3, 20, 18). [ABSTRACT FROM AUTHOR]

We present, in outline, a constructive development of set theory in the style of A.P. Morse's classical counterpart [10]. Since the development is carried in a very precise formal language, it readily lends itself to computer-assisted proof-checking and program extraction from proofs. • A development of constructive set theory in Morse's formal language, which should facilitate both proof checking and program extraction from proofs. • A powerful, general induction theorem. • Discussion of aspects of the proof that the Continuum Hypothesis implies excluded middle. [ABSTRACT FROM AUTHOR]

Let us consider a parametric weighted directed graph in which every arc (j , i) has weight of the form w ((j , i)) = max (P i j + λ , I i j − λ , C i j) , where λ is a real parameter and P , I and C are arbitrary square matrices with elements in R ∪ { − ∞ }. In this paper, we design an algorithm that solves the Non-positive Circuit weight Problem (NCP) on this class of parametric graphs, which consists in finding all values of λ such that the graph does not contain circuits with positive weight. This problem, which generalizes other instances of the NCP previously investigated in the literature, has applications in the consistency analysis of a class of discrete-event systems called P-time event graphs. The proposed algorithm is based on max-plus algebra and formal languages, and improves the worst-case complexity of other existing approaches, achieving strongly polynomial time complexity O (n 4) (where n is the number of nodes in the graph). [ABSTRACT FROM AUTHOR]

Predictability is an important property which is used to predict the failures which is not observable for the sensors straightly before they occur. In an automation system, in addition to the failure caused by a single event, there also exist pattern failures caused by event strings composed of multiple events. In order to prevent some local sites malfunction, the issue of reliable predictability of patterns is considered in this paper, where the prediction information may be distributed at physically separated sites. Our contributions are listed mainly as follows: Firstly, the k -reliable pattern copredictability in decentralized DESs is defined with formal languages. Generally speaking, for a decentralized system where there are r local sites, it is said to be k -reliably pattern copredictable (1 ≤ k ≤ r) if there are at least r − k + 1 local agents which can predict every occurrences of the pattern failure for every pattern failure, it indicates that the prognostication capability will be maintained while r − k local sites in malfunction state. Then two nondeterministic automata respectively named codiagnoser and coverifier from the given system are constructed in this paper, and two algorithms of verifying the reliable copredictability of pattern are presented by constructing the codiagnoser and coverifier respectively for the purpose of attain the capability of prognostication. Especially, two necessary and sufficient conditions under the codiagnoser and coverifier are proposed. Moreover, for the decentralized DESs, the verification algorithm related to the k -reliable pattern copredictability is proposed after presenting the necessary and sufficient conditions for reliable pattern copredictability. It is worth noting that a polynomial complexity algorithm is used in constructing the coverifier and verifying the k -reliable pattern copredictability. • The notion of reliable pattern copredictability in decentralized DESs is proposed. • Algorithms of verifying reliable pattern copredictability of are presented. • Necessary and sufficient condition for reliable pattern copredictability is proposed. [ABSTRACT FROM AUTHOR]

This paper analyzes a new distinguishability operation for finite deterministic machines and languages. The research was inspired by the "Gedanken experiments" on sequential machines performed by Moore in 1956, and extends the study of the unary distinguishability operation to a binary one. Besides studying the new operation's properties, we give a tight bound of its state complexity on regular languages, including the case for finite languages. • We introduce a new binary operation on languages and finite state machines. • We compute the state complexity of this operation for deterministic machines. • The case of incomplete machines and finite languages is also studied. • We prove several properties of the set of minimal distinguishable words. • We improve the results by Moore, and by Shallit for minimal distinguishable words. [ABSTRACT FROM AUTHOR]

• The introduction of formal language requirements for residency and citizenship represents a turning point for integration program teachers' professional identities and conduct. • The association between language proficiency and legal integration affects teachers' sense of agency in adult education. • The strictness and lengthiness of requirements reinforce teachers' perception of reduced agency. • The introduction of formal language requirements entails the negotiation of new teacher roles on a scale between students' and state's agents. This study investigates how language requirements for residency and citizenship influence the professional identities and sense of agency of introduction program language teachers throughout Scandinavia. While Denmark introduced formal language requirements two decades ago, language requirements were effectuated in Norway starting in 2017. In Sweden, requirements have been proposed, but not introduced. The data comprises narrative interviews with 24 experienced language and literacy teachers. Drawing on street-level bureaucracy theory and narrative positioning analysis, the study shows that the introduction of formal requirements represents a turning point in teachers' professional narratives that are recognized as a gradual reduction of agency and a narrowing of the space where professional identities can be negotiated. Whereas the Swedish teachers largely identify as students' agents, Norwegian and Danish language teachers to a larger extent, yet partly unwillingly, negotiate their professional roles at the intersection between policy and professional standards and in dialog with the policy demands. [ABSTRACT FROM AUTHOR]

The circular splicing operation is a language-theoretic operation introduced by Head to model biological phenomena on circular DNA and RNAs. It acts on pairs of circular words under conditions defined by a set of rules. A circular splicing system S is defined by giving an initial set of circular words and a set of rules. S represents a circular language from a generative point of view (splicing language). There are open questions related to the computational power of these systems. For instance, a characterization of circular splicing systems generating regular circular languages is still lacking as well as a characterization of the structure of the regular splicing languages. In this paper we give results about these questions for a special class of hybrid systems named generalized marked systems. [ABSTRACT FROM AUTHOR]

In the software development life cycle, requirements engineering is the main process that is derived from users by informal interviews written in natural language by requirements engineers (analysts). The requirements may suffer from incompleteness and ambiguity when transformed into formal or semi-formal models that are not well understood by stakeholders. Hence, the stakeholder cannot verify if the formal or semi-formal models satisfy their needs and requirements. Another problem faced by requirements is that when code and/or designs are updated, it is often the case that requirements and specifically the requirements document are not updated. Hence ending with a requirements document not reflecting the implemented software. Generating requirements from the design and/or implementation document is seen by many researchers as a way to address the latter issue. This paper presents a survey of some works undertaken in the field of generation natural language specifications from object UML model using the support of an ontology. and analyzing the robustness and limitations of these existing approaches. This includes studying the generation of natural language from a formal model, review the generation of natural language from ontologies, and finally reviews studies about check to generate natural language from OntoUML. [ABSTRACT FROM AUTHOR]

The model of deterministic input-driven multi-counter automata is introduced and studied. On such devices, the input letters uniquely determine the operations on the underlying data structure that is consisting of multiple counters. We study the computational power of the resulting language families and compare them with known language families inside the Chomsky hierarchy. In addition, it is possible to prove a proper counter hierarchy depending on the alphabet size. This means that any input alphabet induces an upper bound which depends on the alphabet size only, such that k + 1 counters are more powerful than k counters as long as k is less than this bound. The hierarchy interestingly collapses at the level of the bound. Furthermore, we investigate the closure properties of the language families. For input-driven multi-counter automata with 0 or 1 counter, we discuss the computational complexity of their decidable problems. For k ≥ 2 counters, the decidability problems of emptiness, finiteness, universality, inclusion, equivalence, regularity, and context-freeness are shown to be non-semidecidable. Finally, we study descriptional complexity aspects of input-driven multi-counter automata. It is shown that a nondeterministic device can be determinized and that 2 n − 1 is a necessary and sufficient blow-up in the number of states for the determinization. For the operational state complexity of deterministic input-driven multi-counter automata under Boolean operations, tight bounds on the number of states are established. Finally, it turns out that the size trade-offs between deterministic input-driven multi-counter automata with k + 1 and k counters are non-recursive, that is, they are not bounded by any recursive function. [ABSTRACT FROM AUTHOR]

We are interested in regular expressions that represent word relations in an alphabet-invariant way—for example, the set of all word pairs (u , v) where v is a prefix of u independently of what the alphabet is. Current software systems of formal language objects do not have a mechanism to define such objects. Labelled graphs (transducers and automata) with alphabet-invariant and user-defined labels were considered in a recent paper. In this paper we study derivatives of regular expressions over labels (atomic objects) in some set B. These labels can be any strings as long as the strings represent subsets of a certain monoid. We show that the number of partial derivatives of any type B regular expression is linearly bounded, and that one can define partial derivative labelled graphs, whose transition labels can be elements of another label set X as long as X and B refer to the same monoid. We also show how to use derivatives directly to decide whether a given word is in the language of a regular expression over set specs. Set specs and pairing specs are label sets allowing one to express languages and relations over large alphabets in a natural and concise way such that many algorithms work directly on these labels without the need to expand these labels to linear or quadratic size expressions. [ABSTRACT FROM AUTHOR]

Context-free grammars are not able to capture cross-serial dependencies occurring in some natural languages. To overcome this issue, Seki et al. introduced a generalization called m -multiple context-free grammars (m -MCFGs), which deal with m -tuples of strings. We show that m -MCFGs are capable of comparing the number of consecutive occurrences of at most 2 m different letters. In particular, the language { a 1 n 1 a 2 n 2 ⋯ a 2 m + 1 n 2 m + 1 | n 1 ≥ n 2 ≥ ... ≥ n 2 m + 1 ≥ 0 } is (m + 1) -multiple context-free, but not m -multiple context-free. [ABSTRACT FROM AUTHOR]

Business process modeling is a key activity during the development of complex and large information systems, such as enterprise management systems. These systems deal with a wide number of business processes; thus, the modeling and validation of processes becomes a challenging task. This entails dealing with issues such as the precedence between tasks and activities within a process, as well as resources, roles and enterprise assets involved. Moreover, undetected mistakes in this phase will be propagated to the system design phase and consequently will have a negative effect in the final system quality. On the other hand, the scientific literature advocates the suitability of formal models to address some issues during the process modeling. However, the adoption of formal models leads to new problems because formal languages are difficult to understand and process stakeholders usually lack of knowledge about them. In that direction, the Model-Driven Architecture (MDA) paradigm includes specifications that may alleviate some difficulties in the adoption of formal languages. Hence, in this paper we introduce an approach which combines MDA-specifications and ontologies to support process modeling. These technologies have great acceptance between both software researchers and developers. The use of ontologies permits to semantically validate the models. Furthermore, the application of MDA-guidelines could facilitate the integration of BPMN, a graphical notation for describing business process models widely accepted among business analysts, with a formal language to automate the analysis of business process models. [ABSTRACT FROM AUTHOR]

We present a weight measure on formal languages based on the summands of a geometric series discounted by the fraction of words of certain length in the language, guaranteeing the weight to be a real value between 0 and 1 for any language. We show that this weight measure is computable for regular languages. As an application, we derive a distance metric between languages as the weight of their symmetric difference and show how it can be used in automatic grading of standard exercises in formal language theory classes. [ABSTRACT FROM AUTHOR]

Graphical depictions of distributed systems' behaviors in the form of Sequence Diagrams (SD) are widely used, with formalisms such as Message Sequence Charts (MSC) or UML-SD. Yet, only restricted subsets of these languages are associated to formal semantics, most of which are given by translation towards other formalisms. These translational approaches are the only ones enabling formal verification thanks to the ecosystem and tools associated to the target formalism. However, traceability of SD concepts is lost and the translation of some operators, in particular the weakly sequential loop, is problematic. In this paper, we define an Interaction Language to encode SD and ground it formally by associating it to three different semantics which we prove to be equivalent. A "denotational" semantics, relying on composing operators over sets of traces (sequences of atomic actions) allows one to reason on algebraic properties of SD. A structural "operational" semantics apprehends SD as executable objects which can express traces one action after the other. It also bridges the gap between the two other semantics and enables proving their equivalence. A functional style "execution" semantics separates two concerns intertwined in the operational semantics that is: identifying immediately executable actions (frontier actions) and computing follow-up SD which specify continuations of behaviors. The use of positions to identify frontier actions resolves non-determinism as every distinct occurrence of these actions have unique positions and are associated to a unique follow-up SD. Additionally, this enables visualizing frontier actions in SD as well as the execution of SD. These three semantics constitute a framework which enable using SD directly for formal verification. Traceability of SD concepts and executed actions is preserved and the weakly sequential loops are treated as any other operator. [ABSTRACT FROM AUTHOR]

Liversedge, Drieghe, Li, Yan, Bai and Hyönä (2016) reported an eye movement study that investigated reading in Chinese, Finnish and English (languages with markedly different orthographic characteristics). Analyses of the eye movement records showed robust differences in fine grained characteristics of eye movements between languages, however, overall sentence reading times did not differ. Liversedge et al. interpreted the entire set of results across languages as reflecting universal aspects of processing in reading. However, the study has been criticized as being statistically underpowered (Brysbaert, 2019) given that only 19–21 subjects were tested in each language. Also, given current best practice, the original statistical analyses can be considered to be somewhat weak (e.g., no inclusion of random slopes and no formal comparison of performance between the three languages). Finally, the original study did not include any formal statistical model to assess effects across all three languages simultaneously. To address these (and some other) concerns, we tested at least 80 new subjects in each language and conducted formal statistical modeling of our data across all three languages. To do this, we included an index that captured variability in visual complexity in each language. Unlike the original findings, the new analyses showed shorter total sentence reading times for Chinese relative to Finnish and English readers. The other main findings reported in the original study were consistent. We suggest that the faster reading times for Chinese subjects occurred due to cultural changes that have taken place in the decade or so that lapsed between when the original and current subjects were tested. We maintain our view that the results can be taken to reflect universality in aspects of reading and we evaluate the claims regarding a lack of statistical power that were levelled against the original article. [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]

• The topological entropy function is surjective. • Languages of deterministic epsilon-free k-counter automata have 0 entropy. • Languages of deterministic epsilon-free k-stack automata have bounded entropy. We introduce the notions of topological entropy of a formal language and of a topological automaton. We show that the entropy function is surjective and bound the entropy of languages accepted by deterministic ε -free push-down automata with an arbitrary amount of stacks. [ABSTRACT FROM AUTHOR]

Constraint LTL over clocks (CLTLoc) is an extension of LTL allowing for atomic formulae of the form x < c or x = c , which constrain the time delay measured by clock x with respect to constant value c. In a previous work, we showed that CLTLoc is equivalent to Timed Automata. The result was proven by considering a clock semantics that conforms to the original definition by Alur and Dill, i.e., when clocks are reset (i.e., equal to 0) in the origin, both CLTLoc and Timed Automata define the class of Timed ω -Regular languages. In this paper, we show that if we allow the clocks to have any value in the origin, the power of the formalism to express timed languages does not change, as long as non-Zeno languages are considered. If Zeno languages are allowed, then CLTLoc is strictly more powerful than TA. As a consequence of these results, we also show that non-Zeno Timed ω -Regular languages are closed with respect to the left quotient operation with timed regular languages over finite words. [ABSTRACT FROM AUTHOR]

We consider several language-theoretic aspects of various notions of unique decipherability (or unique factorization) in formal languages. Given a language L at some position within the Chomsky hierarchy, we investigate the language of words UD (L) in L ⁎ that have unique factorization over L. We also consider similar notions for weaker forms of unique decipherability, such as numerically decipherable words ND (L) , multiset decipherable words MSD (L) and set decipherable words SD (L). Although these notions of unique factorization have been considered before, it appears that the languages of words having these properties have not been positioned in the Chomsky hierarchy up until now. We show that UD (L) , ND (L) , MSD (L) and SD (L) need not be context-free if L is context-free. In fact ND (L) and MSD (L) need not be context-free even if L is finite, although UD (L) and SD (L) are regular in this case. We show that if L is context-sensitive, then so are UD (L) , ND (L) , MSD (L) and SD (L). We also prove that the membership problem (resp., emptiness problem) for these classes is PSPACE-complete (resp., undecidable). We finally determine upper and lower bounds on the length of the shortest word of L ⁎ not having the various forms of unique decipherability into elements of L. [ABSTRACT FROM AUTHOR]

Open-ended text questions provide better assessment of learner's knowledge, but analysing answers for this kind of questions, checking their correctness, and generating of detailed formative feedback about errors for the learner are more difficult and complex tasks than for closed-ended questions like multiple-choice. The analysis of answers for open-ended questions can be performed on different levels. Analysis on character level allows to find errors in characters' placement inside a word or a token; it is typically used to detect and correct typos, allowing to differ typos from actual errors in the learner's answer. The word-level or token-level analysis allows finding misplaced, extraneous, or missing words in the sentence. The semantic-level analysis is used to capture formally the meaning of the learner's answer and compare it with the meaning of the correct answer that can be provided in a natural or formal language. Some systems and approaches use analysis on several levels. The variability of the answers for open-ended questions significantly increases the complexity of the error search and formative feedback generation tasks. Different types of patterns including regular expressions and their use in questions with patterned answers are discussed. The types of formative feedback and modern approaches and their capabilities to generate feedback on different levels are discussed too. Statistical approaches or loosely defined template rules are inclined to false-positive grading. They are generally lowering the workload of creating questions, but provide low feedback. Approaches based on strictly-defined sets of correct answers perform better in providing hinting and answer-until-correct feedback. They are characterised by a higher workload of creating questions because of the need to account for every possible correct answer by the teacher and fewer types of detected errors. The optimal choice for creating automatised e-learning courses are template-based open-ended question systems like OntoPeFeGe, Preg, METEOR, and CorrectWriting which allows answer-until-correct feedback and are able to find and report various types of errors. This approach requires more time to create questions, but less time to manage the learning process in the courses once they are run. [ABSTRACT FROM AUTHOR]

We show that, if S is a finite semiring, then the free profinite S -semimodule on a Boolean Stone space X is isomorphic to the algebra of all S -valued measures on X , which are finitely additive maps from the Boolean algebra of clopens of X to S. These algebras naturally appear in the logic approach to formal languages as well as in idempotent analysis. Whenever S is a (pro)finite idempotent semiring, the S -valued measures are all given uniquely by continuous density functions. This generalises the classical representation of the Vietoris hyperspace of a Boolean Stone space in terms of continuous functions into the Sierpiński space. We adopt a categorical approach to profinite algebra which is based on profinite monads. The latter were first introduced by Adámek et al. as a special case of the notion of codensity monads. [ABSTRACT FROM AUTHOR]

The paper determines the number of states in finite automata necessary to represent "unambiguous" variants of the union, concatenation, and Kleene star operations on formal languages. For the disjoint union of languages represented by an m -state and an n -state deterministic finite automata (DFA), the state complexity is m n − 1 ; for the unambiguous concatenation, it is known to be m 2 n − 1 − 2 n − 2 (Daley et al., "Orthogonal concatenation: language equations and state complexity" , J. UCS , 2010), and this paper shows that this number of states is necessary already over a binary alphabet; for the unambiguous star, the state complexity function is determined to be 3 8 2 n + 1. In the case of a unary alphabet, disjoint union requires up to 1 2 m n states in a DFA, unambiguous concatenation has state complexity m + n − 2 , and unambiguous star requires n − 2 states in the worst case. For nondeterministic finite automata, as well as for unambiguous finite automata, the complexity for disjoint union is m + n , for unambiguous concatenation, square, and star, the resulting complexities are m + n , 2 n , and n + 1 , respectively, and all of them are witnessed by binary languages. In the unary nondeterministic or unambiguous case, the corresponding complexities are m + n for disjoint union, m + n − 1 and 2 n − 1 for unambiguous concatenation and square, respectively, and n − 1 for unambiguous star. [ABSTRACT FROM AUTHOR]

Epigenomics is the study of modifications on the genetic material of a cell that do not depend on changes in the DNA sequence, since those latter involve specific proteins around which DNA wraps. The end result is that Epigenomic changes have a fundamental role in the proper working of each cell in Eukaryotic organisms. A particularly important part of Epigenomics concentrates on the study of chromatin, that is, a fiber composed of a DNA-protein complex and very characterizing of Eukaryotes. Understanding how chromatin is assembled and how it changes is fundamental for Biology. In more than thirty years of research in this area, Mathematics and Theoretical Computer Science have gained a prominent role, in terms of modeling and mining, regarding in particular the so-called 10 nm fiber. Starting from some very basic notions of Biology, we briefly illustrate the recent advances obtained via laboratory experiments on the organization and dynamics of chromatin. Then, we mainly concentrate our attention on the contributions given by Combinatorial and Informational Methodologies, that are at the hearth of Theoretical Computer Science, to the understanding of mechanisms determining the 10 nm fiber. We conclude highlighting several directions of investigation that are perceived as important and where Theoretical Computer Science can provide high impact results. [ABSTRACT FROM AUTHOR]

Analogs of balls in n -dimensional Euclidean space are defined in the monoid of strings composed of letters of an alphabet if a metric is defined on the monoid. These analogs are not only balls in the monoid of strings but also regular languages. Since the Levenshtein distance, a reasonable metric between strings, was introduced in 1965, researchers have aimed to determine a formula for computing the volumes of balls of strings under this distance and their growth rate. However, this problem remains open. In this paper, we first derive a formula for the volumes of balls of strings under a metric obtained by extending the Hamming distance as a metric on the whole monoid and subsequently reveal the growth rate of balls of strings under the Levenshtein distance using this formula. Furthermore, we describe a conjecture on the formula for the volumes of spheres of strings under the Levenshtein distance. Next, we construct an efficient randomized algorithm that computes estimates of the volumes of the balls whose estimation errors are less than a given value with a probability greater than a specified value. Finally, we examine the validity of the proposed conjecture, using the (true) volumes obtained by exhaustive searches for small spheres and estimates of the volumes obtained by this algorithm for large ones. [ABSTRACT FROM AUTHOR]

Modelling and Analysing Cyber–Physical Systems (CPS) is a challenge for Formal Methods and therefore a field of active research. It is characteristic of CPSs that models comprise aspects of Newtonian Physics appearing in system environments, the difficulties of their discretization, the problems of communication and interaction between actors in this environment as well as calculations respecting time-bounds. We present a novel framework to address these problems developed with industrial partners involved in the Autonomous Car domain. Based on HOL-CSP, we model time, physical evolution, "scenes" (global states) and "scenarios" (traces) as well as the interaction of "actors" (vehicles, pedestrians, traffic lights) inside this framework. In particular, discrete samplings are modelled by infinite internal choices. For several instances of the modelling framework, we give formal proofs of a particular safety property for Autonomous Cars: if each car follows the same driving strategy defined by the so-called Responsibility-Sensitive Safety (RSS), no collision will occur. The proofs give rise to a number of variants of RSS and optimizations as well as a test-case partitioning of abstract test cases and a test-strategy for integration tests. • Modelling and Analysing Cyber–Physical Systems (CPS) is a challenge for Formal Methods and therefore a field of active research. • We present a novel approach to specify CPS in a very expressive formal specification language HOL-CSP (based as conservative theory development on Isabelle/HOL) geared towards time-triggered modelling. • Formal Analysis of CPS models can be done by semi-automated proofs in Isabelle. • We present a larger case-study over the safety of a driving strategy stemming from the autonomous car domain. [ABSTRACT FROM AUTHOR]

Accessing the large volumes of information available in public knowledge bases might be complicated for those users unfamiliar with formal languages, such as the SPARQL query language and the ontology definition languages. This issue can be overcome by providing systems able to answer questions posed in natural language on a knowledge base, a task that is called Knowledge Base Question Answering (KBQA) in the literature. More in detail, many KBQA systems aim at translating automatically questions into the corresponding SPARQL queries to be executed over the knowledge base to get the answers. Effective state-of-the-art KBQA systems are based on neural-machine translation but easily fail to recognize words that are Out Of the Vocabulary (OOV) of the training set. This is a serious issue while querying large ontologies where the list of entities is huge and easily evolves over time. In this paper, we present the SPARQL-QA-v2 system that combines in an innovative way Named Entity Linking, Named Entity Recognition, and Neural Machine Translation for addressing the problem of generating SPARQL queries from questions posed in natural language. We demonstrate empirically that SPARQL-QA-v2 is effective and resilient to OOV words and delivers state-of-the-art performance in well-known datasets for question answering over DBpedia and Wikidata knowledge bases. • NMT-based approach resilient to out-of-vocabulary words for KBQA. • Combination of novel NLP dedicated tools. • Experimental analysis in well-known datasets for Knowledge Base Question Answering. • Winner of the 10th Question Answering over Linked Data (QALD) Challenge at ESCW 2022. [ABSTRACT FROM AUTHOR]

According to the Language of Thought Hypothesis (LoTH), an influential account in philosophy and cognitive science, human cognition is underlain by symbolic reasoning in a formal language. In this account, concepts are expressions in a Language of Thought, deduction is syntactic manipulation in this language, and learning is an inference of expressions in this language from data. This picture raises the question of what LoT humans have, and how to infer it from behavior. In this paper, we pave the way towards answering this question, by approaching a more fundamental question: to what extent is it possible in principle to recover the human LoT from experimental data? To answer this question, we focus on the fragment of LoT that is concerned with representing Boolean categories and simulate the recovery of the Boolean LoT from category learning experiments. Our findings show that in principle the vast majority of Boolean LoTs can be accurately recovered from experimental data. However, we find that this crucially depends on the employed experimental design. Moreover, we find evidence that LoTs with fewer operators can be recovered from category learning data faster. [ABSTRACT FROM AUTHOR]

We define a notion of randomness for individual and collections of formal languages based on automatic martingales acting on sequences of words from some underlying domain. An automatic martingale bets if the incoming word belongs to the target language or not. Then randomness of both single languages and collections of languages is defined as a failure of automatic martingale to gain an unbounded capital by betting on the target language according to an incoming sequence of words, or a text. The randomness of formal languages turned out to be heavily dependent on the text. For very general classes of texts, any nonregular language happens to be random when considered individually. As for collections of languages, very general classes of texts permits nonrandomness of automatic families of languages only. On the other hand, an arbitrary computable language is shown to be nonrandom under certain dynamic texts. [ABSTRACT FROM AUTHOR]

Edit distance ℓ -neighbourhood of a formal language is the set of all strings that can be transformed to one of the strings in this language by at most ℓ insertions and deletions. Both the regular and the context-free languages are known to be closed under this operation, whereas the family recognized by deterministic pushdown automata is not. This paper establishes the closure of the family recognized by input-driven pushdown automata (IDPDA), also known as visibly pushdown automata, under the edit distance neighbourhood operation. For an n -state nondeterministic IDPDA with n stack symbols, an automaton for its edit distance ℓ -neighbourhood using O (n ℓ + 1) states is constructed, and an asymptotically matching lower bound is established. For an n -state deterministic IDPDA, its 1-neighbourhood in the worst case requires a deterministic IDPDA with at least 2 Ω (n 2) states. [ABSTRACT FROM AUTHOR]

A picture, or two-dimensional (2D) string, is a rectangular array of symbols over a finite alphabet. In this paper, we introduce the notion of fullness for sets of strings and sets of pictures. Fullness is a local counterpart of completeness. While in 1D fullness coincides with completeness, in 2D complete sets of pictures are a subset of full ones. This new notion allows introducing the encoding of a picture. The definition of encoding is based on the one of cutting decomposition. If a set of pictures X is full then any picture has an encoding over X ; furthermore, the encoding is unique if X is a univocally full set. Univocally full sets coincide with the maximal strong prefix codes of pictures that were recently introduced. At last, we show an encoding algorithm for pictures, which relies on a new tree data structure to represent univocally full sets. [ABSTRACT FROM AUTHOR]

For a closure operation c and an involution i defined on a language family L , we define N c , i L (L) as the number of languages which can be obtained from L by repeated applications of c and i. The orbit O L (c , i) of c and i is defined as the set of all these numbers. We determine the orbit for some classical language theoretic closure operators and the involution complement. We show that complement and reversal behave very different with respect to some special closure operators. Moreover, we prove that, for an arbitrary closure operator and reversal, some "small" numbers cannot be avoided in the orbit. [ABSTRACT FROM AUTHOR]

I argue that the ability to compute phrase structure grammars is indicative of a particular kind of thought. This type of thought that is only available to cognitive systems that have access to the computations that allow the generation and interpretation of the structural descriptions of phrase structure grammars. The study of phrase structure grammars, and formal language theory in general, is thus indispensable to studies of human cognition, for it makes explicit both the unique type of human thought and the underlying mechanisms in virtue of which this thought is made possible. • Phrase structure grammars are indicative of uniquely human thoughts. • Such thoughts are only available to beings that can compute PSGs. • Research suggests that only humans can compute PSGs. • It follows that thoughts made possible by PSGs are uniquely human. • Formal language theory is thus indispensable to studies of cognition. [ABSTRACT FROM AUTHOR]

Abstract This paper introduces sets of binary subtree representations as an alternative to shared packed parse forests as the output of a generalised parser, and shows how these may be generated by Earley's algorithm, by a new GLL-style parser and by Johnson's continuation passing combinator style parsers. The set based output removes the clerical overhead associated with graph constructions, making the parsers simpler. Highlights • Introduces BSR sets, an alternative to the SPPF representation of all derivations of a string. • General BSR combinator parsers and Earley-style parsers are presented. • A new BSR GLL-style parser (CNP) is presented which has a more efficient combined call stack. • Data structure size comparisons for GLL and CNP are given for C, C++ and Java grammars. [ABSTRACT FROM AUTHOR]

Highlights • The methodology allowed for an emic analysis from both participants' perspectives. • The analysis allowed to discern if troubles of intersubjectivity concern "lag". • "Lag" delays transition-relevance places in video-mediated environments. • Participants handle "lag" better when interactional roles are clearly defined. • Participants use practices related to turn design and construction to manage "lag". Abstract The purpose of this article is to describe tandem dyads' interactional resources and social practices for upholding intersubjectivity in video-mediated environments (VMEs) within the context of tandem language learning in a virtual learning environment (eClassroom tandem) arranged within formal language education in upper secondary schools. Data consists of video and screen recordings of several tandem dyads' video-mediated interaction. Using conversation analysis, the study analyses how "lag" (a delay in the connection) affects participants' meaning-making and ways to maintain intersubjectivity in VMEs. The results show that participants use different interactional resources and practices regarding turn-taking, turn design, and turn construction to maintain intersubjectivity. Clearly defined conversational roles in the assignments appear to help participants to cope with delays. Additionally, in the context of eClassroom tandem, the roles of the L1 speaker and the L2 speaker appear to be of situated importance for upholding a mutual understanding in VMEs. [ABSTRACT FROM AUTHOR]

Abstract Medical processes combine medical actions which are performed by health care professionals while they observe signs and symptoms and decide about interventions, prescriptions, or tests, in order to deal with the health problem that affects a particular patient. Our research was centered in the representation of knowledge for the purpose of decision making in medical processes for chronic diseases. In order to achieve this objective, we followed three steps: (1) We performed an analysis and comparison of formal languages for procedural knowledge representation from a decision-making perspective. (2) We proposed an intuitive, easy, and effective mechanism of medical knowledge formalization. And, (3) we defined a methodology to model medical processes. Our new formalism to represent knowledge is called the extended Timed Transition Diagram (eTTD) and can be used to describe three basic levels of decision making in a long-term treatment: therapy strategy, dosage, and intolerances. The methodology can be applied manually to build eTTDs from clinical practice guidelines (CPGs) or automatically to construct them using the information available in clinical records about individual, multi-level medical processes. We validated eTTDs with clinical practice guidelines for arterial hypertension. The obtained models can be used as a baseline framework for medical, procedural decision support systems development. Highlights • Comparison of formal languages for procedural knowledge representation is provided. • An intuitive and effective mechanism of medical knowledge formalization is proposed. • A methodology to model medical procedures from individual, multi-level, medical processes is proposed. • Extended Timed Transition Diagram represents three basic levels of decision-making. • Models of therapeutic strategy, drug titration, and drug intolerances are obtained. [ABSTRACT FROM AUTHOR]

Abstract Let G be a group and let φ : Σ ⁎ → G be a monoid homomorphism from the set of all strings Σ ⁎ over some finite alphabet Σ onto the group G. The set Σ is then called a generating set for G and the language { 1 } φ − 1 ⊆ Σ ⁎ is called the word problem of G with respect to the generating set Σ (via the homomorphism φ) and is denoted by W (G , Σ). We consider nine conditions that hold in each such language of the form W (G , Σ) and determine which combinations of these conditions are equivalent to the property of the language in question being the word problem of a group. We show that each of these nine conditions is decidable for the family of regular languages but that each is undecidable for the family of one-counter languages (the languages accepted by one-counter pushdown automata). We also show that the property of a language being the word problem of a group is undecidable for the family of one-counter languages but is decidable for the family of deterministic context-free languages (the languages accepted by deterministic pushdown automata). [ABSTRACT FROM AUTHOR]

This paper presents formalizations that capture definitions of a number of concepts of the ISO/IEC 15504-5 process assessment model and the CMMI v1.3 constellations process models and relations among the concepts. The formalizations are expressed in a formal language, OWL. The main objectives for these formalizations are to be consistent with the ISO/IEC 15504-5 process assessment model and the CMMI-DEV/SVC/ACQ v1.3 models and to be effective, i.e., to allow for an automatic determination of an organizations maturity level and of a process capability level based upon data collected during an assessment. The formalizations are presented in a number of levels, from more general concepts to more specific. To assess the validity of the ISO/IEC 15504-5 formalization, a number of test cases for the scenario of automatic determination of the capability levels were developed. To assess the validity of the CMMI v1.3 formalizations, a number of real cases were selected from the CMMI institute published appraisal results with the purpose of validating the automatic determination of both organizational maturity and process areas capability levels. A set of OWL reasoners were then used to derive the capability levels for a specific process group (regarding the ISO/IEC 15504-5) and to derive the organizational maturity and process areas capability levels for the CMMI-DEV v1.3 constellation. While the test results were all positive, the real value of these formalizations comes from the fact that they faithfully captured the main aspects of ISO/IEC 15504-5 and CMMI v1.3, both well established and accepted models for the assessment of organizational processes, and that an inference engine was able to support the assessment of processes capability levels and of organizations maturity levels. [ABSTRACT FROM AUTHOR]

Abstract It is well known that the “store language” of every pushdown automaton — the set of store configurations (state and stack contents) that can appear as an intermediate step in accepting computations — is a regular language. Here many models of language acceptors with various store structures are examined, along with a study of their store languages. For each model, an attempt is made to find the simplest model that accepts their store languages. Some connections between store languages of one-way and two-way machines are demonstrated, as with connections between nondeterministic and deterministic machines. A nice application of these store language results is also presented, showing a general technique for proving families accepted by many deterministic models are closed under right quotient with regular languages, resolving some open questions (and significantly simplifying proofs for others that are known) in the literature. Lower bounds on the space complexity of Turing machines for having non-regular store languages are obtained. [ABSTRACT FROM AUTHOR]