Humans make mistakes, especially when faced to complex tasks, such as the construction of modern hardware or software. This thesis focuses on machine-assisted techniques to guarantee that computers behave correctly. Modern computer systems are large and complex. Automated formal verification stands as an alternative to testing or simulation to ensuring their reliability. It essentially proposes to employ computers to exhaustively check the system behavior. Unfortunately, automated verification suffers from the state-space explosion problem: even relatively small systems can reach a huge number of states. Using the right representation for the system behavior seems to be a key step to tackle the inherent complexity of the problems that automated verification solves. The verification of concurrent systems poses additional issues, as their analysis requires to evaluate, conceptually, all possible execution orders of their concurrent actions. Petri net unfoldings are a well-established verification technique for concurrent systems. They represent behavior by partial orders, which not only is natural but also efficient for automatic verification. This dissertation focuses on the verification of concurrent systems, employing Petri nets to formalize them, and studies two prominent verification techniques: model checking and fault diagnosis. We investigate the unfoldings of Petri nets extended with read arcs. The unfoldings of these so-called contextual nets seem to be a better representation for systems exhibiting concurrent read access to shared resources: they can be exponentially smaller than conventional unfoldings on these cases. Theoretical and practical contributions are made. We first study the construction of contextual unfoldings, introducing algorithms and data structures that enable their efficient computation. We integrate contextual unfoldings with merged processes, another representation of concurrent behavior that alleviates the explosion caused by non-determinism. The resulting structure, called contextual merged processes, is often orders of magnitude smaller than unfoldings, as we experimentally demonstrate. Next, we develop verification techniques based on unfoldings. We define SAT encodings for the reachability problem in contextual unfoldings, thus solving the problem of detecting cycles of asymmetric conflict. Also, an unfolding-based decision procedure for fault diagnosis under fairness constraints is presented, in this case only for conventional unfoldings. Finally, we implement our verification algorithms, aiming at producing a competitive model checker intended to handle realistic benchmarks. We subsequently evaluate our methods over a standard set of benchmarks and compare them with existing unfolding-based techniques. The experiments demonstrate that reachability checking based on contextual unfoldings outperforms existing techniques on a wide number of cases. This suggests that contextual unfoldings, and asymmetric event structures in general, have a rightful place in research on concurrency, also from an efficiency point of view.

Orientador: Marcelo Esteban Coniglio / Tese (doutorado) - Universidade Estadual de Campinas, Instituto de Filosofia e Ciências Humanas / Made available in DSpace on 2018-08-17T19:11:26Z (GMT). No. of bitstreams: 1 Silvestrini_LuizHenriquedaCruz_D.pdf: 1289416 bytes, checksum: aa5f4929e7149a647d28c4fd4df86874 (MD5) Previous issue date: 2011 / Resumo: Mikenberg, da Costa e Chuaqui (1986) introduziram a noção de quase-verdade por meio da noção de estruturas parciais, e para tanto, conceberam os predicados como ternas. O arcabouço conceitual resultante proporcionou o emprego de estruturas parciais na ciência, pois, em geral, não sabemos tudo a respeito de um determinado domínio de conhecimento. Generalizamos a noção de predicados como ternas para fórmulas complexas. A partir desta nova abordagem, obtemos uma definição de quase-verdade via noção de satisfação pragmática de uma fórmula A em uma estrutura parcial E. Introduzimos uma lógica subjacente à nossa nova definição de quase-verdade, a saber, a lógica paraconsistente trivalente LPT1, a qual possui uma axiomática de primeira ordem. Relacionamos a noção de quase-verdade com algumas lógicas paraconsistentes já existentes. Defendemos que a formalização das Sociedades Abertas, introduzidas por Carnielli e Lima-Marques (1999), quando combinada com quantificadores modulados, introduzidos por Grácio (1999), constitui uma alternativa para capturar a componente indutiva presente na atividade científica, e mostramos, a partir disso, que a proposta original de da Costa e colaboradores pode ser explicada em termos da nova noção de sociedades moduladas / Abstract: Newton da Costa and his collaborators have introduced the notion of quasi-truth by means of partial structures, and for this purpose, they conceived the predicates as ordered triples: the set of tuples which satisfies, does not satisfy and can satisfy or not the predicate, respectively (the latter represents lack of information). This approach provides a conceptual framework to analyse the use of (first-order) structures in science in contexts of informational incompleteness. In this Thesis, the notion of predicates as triples is extended recursively to any complex formula of the first-order object language. From this, a new definition of quasi-truth via the notion of pragmatic satisfaction is obtained. We obtain the proof-theoretic counterpart of the logic underlying our new definition of quasi-truth, namely, the three-valued paraconsistent logic LPT1, which is presented axiomatically in a first-order language. We relate the notion of quasi-truth with some existing paraconsistent logics. We defend that the formalization of (open) society semantics when combined with the modulated quantifiers constitutes an alternative to capture the inductive component present in scientific activity, and show, from this, that the original proposal of da Costa and collaborators can be explained in terms of the new concept of modulated societies / Doutorado / Filosofia / Doutor em Filosofia

M.Sc. / In this thesis we study some of the propertie of a clas called automatic structures. Automatic structures are structures that can be encoded (in some defined way) into a set of regular languages. This encoding allows one to prove many interesting properties about automatic structures, including decidabilty results.

Medication prescriptions constitute an important type of clinical intervention. Medication adherence is the degree to which a patient consumes their medication as agreed upon with a prescriber. Despite many years of research, medication non-adherence continues to be a problem of note, partially due to its multi-faceted in nature. Numerous interventions have attempted to improve adherence but none have emerged as definitive. A significant sub-problem is the lack of consensus regarding definitions and measurement of adherence. Several recent reviews indicate that discrepancies in definitions, measurement techniques, and study methodologies make it impossible to draw strong conclusions via meta-analyses of the literature. Technological interventions aimed at improving adherence have been the subject of ongoing research. Due to the increasing prevalence of the Internet of Things, technology can be used to provide a continuous stream of data regarding a patient's behaviour. To date, several researchers have proposed interventions that leverage data from the Internet of Things, however none have established an acceptable means of analyzing and acting upon this wealth of data. This thesis introduces a computational definition for adherence that can be used to support continued development of technological adherence interventions. A central part of the proposed definition is a formal language for specifying prescriptions that uses fuzzy set theory to accommodate imprecise concepts commonly found in natural language medication prescriptions. A prescription specified in this language can be transformed into an evaluation function which can be used to score the adherence of a given medication taking behaviour. Additionally, the evaluator function is applied to the problem of scheduling medication administrations. A compiler for the proposed language was implemented and had its breadth of expression and clinical accuracy evaluated. The results indicate that the proposed computational definition of adherence is acceptable as a proof of concept and merits further works. / Graduate

This paper deals with a connection between two decision problems for recognizable trace languages: the star problem and the finite power property problem. Due to a theorem by Richomme from 1994 [26, 28], we know that both problems are decidable in trace monoids which do not contain a C4 submonoid. It is not known, whether the star problem or the finite power property are decidable in the C4 or in trace monoids containing a C4. In this paper, we show a new connection between these problems. Assume a trace monoid IM (Σ, I) which is isomorphic to the Cartesian Product of two disjoint trace monoids IM (Σ1, I1) and IM (Σ2, I2). Assume further a recognizable language L in IM (Σ, I) such that every trace in L contains at least one letter in Σ1 and at least in one letter in Σ2. Then, the main theorem of this paper asserts that L* is recognizable iff L has the finite power property.

Software product line engineering is a common method for designing complex software systems. Feature modeling is the most common approach to specify product lines. A feature model is a feature diagram (a special tree of features) plus some crosscutting constraints. Feature modeling languages are grouped into basic and cardinality-based models. The common understanding of the semantics of feature models is a Boolean semantics. We discuss a major deficiency of this semantics and fix it by applying, in turn, modal logic, the theory of multisets, and formal language theory. In order to adequately represent the semantics of basic models, we propose a Kripke semantics and show that basic feature modeling needs a modal rather than Boolean logic. We propose two multiset based theories for cardinality-based feature diagrams, called flat and hierarchical semantics. We show that the hierarchical semantics of a given cardinality-based diagram captures all information in the diagram. We also charac- terize sets of multisets, which can provide a hierarchical semantics of some diagrams. We provide three different reduction processes going from a cardinality-based diagram to an appropriate regular expression. As for crosscutting constraints, we propose a formal language interpretation of them. We also characterize some existing analysis operations over feature models in terms of operations on the corresponding languages and discuss the relevant decidability problems. / Thesis / Doctor of Philosophy (PhD)

<p>This thesis concerns itself with drawing out some interesting connections between the fields of group theory and formal language theory. Given a group with a finite set of generators, it is natural to consider the set of generators and their inverses as an alphabet. We can then consider formal languages such that every group element has at least one representative in the language. We examine what the structure of the language can tell us about group theoretic properties, focusing on the word problem, automatic structures on groups, and generalizations of automatic structures. Finally we prove new results concerning applications of languages of nested words for studying the word problem.</p> / Master of Science (MSc)

The material taught in a Formal Languages course is mathematical in nature and requires students to practice proofs and algorithms to understand the content. Traditional Formal Languages textbooks are heavy on prose, and homework typically consists of solving many paper exercises. Some instructors make use of finite state machine simulators like the JFLAP package. JFLAP helps students by allowing them to build models and apply various algorithms on these models, which improves student interaction with the studied material. However, students still need to read a significant amount of text and practice problems by hand to achieve understanding. Inspired by the principles of the Programmed Instruction (PI) teaching method, we seek to develop a new Formal Languages eTextbook capable of conveying these concepts more intuitively. The PI approach has students read a little, ideally a sentence or a paragraph, and then answer a question or complete an exercise related to that information. Based on the question response, students can continue to other information frames or retry to solve the exercise. Our goal is to present all algorithms using algorithm visualizations and produce proficiency exercises to let students demonstrate understanding. To evaluate the pedagogical effectiveness of our new eTextbook, we conduct time and performance evaluations across two offerings of the course CS4114 Formal Languages and Automata. In time evaluation, the time spent by students looking at instructional content with text and visualizations versus with PI frames is compared to determine levels of student engagement. In performance evaluation, students grades are compared to assess learning gains with text and paper exercises only, with text, visualizations with exercises, and with PI frames. / Doctor of Philosophy / Theory textbooks in computer science are hard to read and understand. Traditionally, instructors use books that are heavy on mathematical prose and paper exercises. Sometimes, instructors use simulators to allow students to create, simulate, and test models. Previously, we found that students tend to skip reading the text presented in the books. This leads to less understanding of the topics taught in the course. To increase student engagement, we developed a new eTextbook for the Formal Languages course. We used pedagogy based on Programmed Instruction, presenting the content in the form of short bits of prose followed by the related question. If students can solve the question correctly, this means that they understood the content and are ready to move forward. To help both instructors and students, we developed a new Formal Languages simulator named OpenFLAP. OpenFLAP allows instructors to create many exercises, and OpenFLAP can grade these exercises automatically.

Orientador: Itala Maria Loffredo D'Ottaviano / Tese (doutorado) - Universidade Estadual de Campinas, Instituto de Filosofia e Ciencias Humanas / Made available in DSpace on 2018-09-11T21:14:41Z (GMT). No. of bitstreams: 1 Bueno-Soler_Juliana_D.pdf: 1230879 bytes, checksum: c04ce9e8061c154854f6283749f9c12b (MD5) Previous issue date: 2009 / Resumo: O presente trabalho tem por objetivo investigar o papel da negação no âmbito das modalidades, de forma a poder esclarecer até que ponto a negação pode ser atenuada, controlada ou mesmo totalmente eliminada em favor da melhor expressabilidade lógica de certas teorias, asserções ou raciocínios que sofrem os efeitos da negação. Contudo, atenuar ou eliminar a negação tem um alto preço: métodos tradicionais em lógica podem deixar de ser válidos e certos resultados, como teoremas de completude para sistemas lógicos, podem ser derrogados. Do ponto de vista formal, a questão central que investigamos aqui e até que ponto tais métodos podem ser restabelecidos. Com tal finalidade, iniciamos nosso estudo a partir do que denominamos sistemas anódicos" (sem negação) e, a posteriori, introduzimos gradativamente o elemento catódico" (negações, com diversas gradações e diferentes características) nos sistemas modais por meio de combinações com certas lógicas paraconsistentes, as chamadas lógicas da inconsistência formal (LFIs). Todos os sistemas tratados são semanticamente caracterizados por semânticas de mundos possíveis; resultados de incompletude são também obtidos e discutidos. Obtemos ainda semânticas modais de traduções possíveis para diversos desses sistemas. Avançamos na direção das multimodalidades, investigando os assim chamados sistemas multimodais anódicos e catódicos. Finalmente, procuramos avaliar criticamente o alcance e o interesse dos resultados obtidos na direção da racionalidade sensível à negação. / Abstract: The present work aims to investigate the role of negations in the scope of modalities and in the reasoning expressed by modalities. The investigation starts from what we call anodic" systems (without any form of negation) and gradually reaches the cathodic" elements, where negations are introduced by means of combining modal logics with certain paraconsistent logics known as logics of formal inconsistency (LFIs). We obtain completeness results for all treated systems, and also show that certain incompleteness results can be obtained. The class of the investigated systems includes all normal modal logics that are extended by means of the schema Gk;l;m;n due to E. J. Lemmon and D. Scott combined with LFIs. We also tackle the question of obtaining modal possible-translations semantics for these systems. Analogous results are analyzed in the scope of multimodalities, where anodic as much as cathodic logics are studied. Finally, we advance a critical evaluation of the reach and scope of all the results obtained to what concerns expressibility of reasoning considered to be sensible to negation. We also critically assess the obtained results in contrast with problems of rationality that are sensible to negation. / Doutorado / Doutor em Filosofia

O avanço tecnológico recente tem atraído tanto a comunidade acadêmica quanto o mercado para a investigação de novos métodos, técnicas e linguagens formais para a área de Projeto de Engenharia. A principal motivação é o atendimento à demanda para desenvolver produtos e sistemas cada vez mais completos e que satisfaçam as necessidades do usuário final. Necessidades estas que podem estar ligadas, por exemplo, à análise e reconhecimento de objetos que compõe uma imagem pela sua textura, um processo essencial na automação de uma enorme gama de aplicações como: visão robótica, monitoração industrial, sensoriamento remoto, segurança e diagnóstico médico assistido. Em vista da relevância das inúmeras aplicações envolvidas e pelo fato do domínio de aplicação ser muito próximo do contexto do desenvolvedor, é apresentada uma proposta de um processo de design baseado no Projeto Axiomático como sendo o mais indicado para esta situação. Especificamente, se espera que no estudo de caso da análise de textura haja uma convergência mais rápida para a solução - se esta existir. No estudo de caso, se desenvolve uma nova concepção de arquitetura de rede neural artificial (RNA), auto-organizável, com a estrutura espacial bidimensional da imagem de entrada preservada, tendo a extração e reconhecimento/classificação de textura em uma única fase de aprendizado. Um novo conceito para o paradigma da competição entre os neurônios também é estabelecida. O processo é original por permitir que o desenvolvedor assuma concomitantemente o papel do cliente no projeto, e especificamente por estabelecer o processo de sistematização e estruturação do raciocínio lógico do projetista para a solução do problema a ser desenvolvido e implementado em RNA. / The recent technological advance has attracted the industry and the academic community to research and propose methods, seek for new techniques, and formal languages for engineering design in order to respond to the growing demand for sophisticated product and systems that fully satisfy customers needs. It can be associated, for instance, with an application of object recognition using texture features, essential to a variety of applications domains, such as robotic vision, industrial inspection, remote sensing, security and medical image diagnosis. Considering the importance of the large number of applications mentioned before, and due to their characteristic where both application and developer domain are very close to each other, this work aims to present a design process based on ideas extracted from axiomatic design to accelerate the development for the classical approach to texture analysis. Thus, a case study is accomplished where a new conception of neural network architecture is specially designed for the following proposal: preserving the two-dimensional spatial structure of the input image, and performing texture feature extraction and classification within the same architecture. As a result, a new mechanism for neuronal competition is also developed as specific knowledge for the domain. In fact, the process proposed has some originality because it does take into account that the developer assumes also the customers role on the project, and establishes the systematization process and structure of logical reasoning of the developer in order to develop and implement the solution in neural network domain.