1,720,966 research outputs found
Apprentissage et vérification de systèmes complexes avec des spécifications temporelles
No full textAu cours de la dernière décennie, on a assisté à une augmentation sans précédent de l'incorporation de systèmes cyber-physiques complexes utilisés pour effectuer des tâches complexes. La vérification de ces systèmes est nécessaire pour garantir leur sécurité et leur fiabilité, en particulier dans les scénarios de sécurité critiques. La vérification formelle s'est avérée être une méthode éprouvée pour vérifier systématiquement ces systèmes. Elle fournit notamment des techniques permettant de contrôler l'exécution des systèmes par rapport à une spécification formelle. Souvent, ces spécifications sont difficiles à concevoir manuellement, d'où la nécessité de les générer automatiquement à partir des exécutions du système pour les utiliser à des fins de vérification. La logique temporelle a gagné en popularité en tant que spécification formelle en raison de sa rigueur mathématique, de son interprétabilité par l'homme et de sa compatibilité avec diverses techniques de vérification formelle. L'objectif de cette thèse est double : (i) Développer des algorithmes pour apprendre automatiquement des spécifications temporelles à partir d'exécutions de systèmes ; (ii) Appliquer des techniques de vérification formelle pour évaluer l'exactitude du système par rapport aux spécifications acquises.Pour atteindre ces objectifs, dans la partie apprentissage, nous présentons deux algorithmes pour apprendre des spécifications dans des logiques temporelles telles que LTL, MTL et STL. Nos algorithmes sont dans le cadre de l'apprentissage passif et apprennent des spécifications qui séparent un ensemble fini de comportements positifs du système d'un ensemble fini de comportements négatifs. Pour les spécifications LTL, nous présentons un algorithme basé sur la programmation dynamique qui s'appuie sur une forme normale pour un fragment de LTL et utilise des techniques d'énumération efficaces pour apprendre des formules concises à partir des exécutions du système. Pour MTL et STL, nous développons des techniques basées sur un résolveur SMT pour apprendre des formules qui sont non seulement concises mais aussi efficaces pour être appliquées à la vérification formelle du système. Nos algorithmes sont mis en œuvre dans des outils appelés SCARLET et TEAL, et leur efficacité est démontrée par des résultats expérimentaux. Pour la partie vérification, nous nous concentrons sur les problèmes de synthèse de paramètres LTL des One-counter automata, qui est l'un des modèles formels fondamentaux pour représenter les systèmes complexes, à savoir les systèmes avec un espace d'état discret mais infini. One-counter automata sont obtenus en étendant les automates classiques à états finis avec un compteur dont la valeur peut s'étendre sur des entiers non négatifs et être testée pour zéro. Les mises à jour et les tests applicables au compteur peuvent être paramétrés en introduisant un ensemble de variables à valeur entière appelées paramètres. Le problème de la synthèse des paramètres LTL pour de tels automates est de savoir s'il existe une évaluation des paramètres telle que toutes les exécutions infinies de l'automate satisfont une spécification LTL. En s'appuyant sur les travaux existants dans la littérature, (i) nous montrons un réencodage prudent du problème en une restriction décidable de l'arithmétique de Presburger avec divisibilité (PAD), le plus grand fragment décidable connu de PAD jusqu'à présent ; (ii) Nous prouvons que le problème de la synthèse des paramètres est décidable en général et en 3NEXP ; (iii) Nous donnons des algorithmes EXPSPACE pour les cas particuliers du problème où les paramètres ne peuvent être utilisés que dans des contre-tests. Enfin, (iv) nous présentons brièvement le résultat de décidabilité de ce problème sur une extension de ce modèle avec des contraintes de Parikh.In the past decade, there has been an unprecedented rise in the incorporation of complex cyber-physical systems being used in performing complex tasks. Verification of these systems is necessary to ensure the safety and reliability of these systems, especially in safety-critical scenarios. Formal verification has been proven to be a time-tested method to systematically verify these systems. In particular, it provides techniques for monitoring system executions against a formal specification. Often, these specifications are hard to design manually, necessitating a need to automatically generate them from system executions to be used for verification purposes. Temporal logic has gained popularity as a formal specification due to its mathematical rigour, human interpretability, and compatibility with various formal verification techniques. The objective of this thesis is twofold: (i) Develop algorithms to automatically learn temporal specifications from system executions; (ii) Apply formal verification techniques to assess the correctness of the system against the acquired specifications.To achieve these objectives, in the learning part, we present two algorithms to learn specifications in temporal logics such as LTL, MTL and STL. Our algorithms are in emph{passive learning} setting that learn specifications that separate a finite set of positive system behaviours from a finite set of negative ones. For LTL specifications, we present a dynamic programming based algorithm that leverages a normal form for a fragment of LTL and uses efficient enumeration techniques to learn concise formulas from system executions. For MTL and STL, we develop SMT-solver based techniques to learn formulas that are not only concise but also efficient to be applied for formal verification of the system. Our algorithms are implemented in tools called SCARLET and TEAL, and their efficiency is demonstrated through experimental results. For the verification part, we focus on the LTL parameter-synthesis problems of one-counter automata, which is one of the fundamental formal models to represent complex systems, namely systems with discrete yet infinite state space. One-counter automata are obtained by extending classical finite-state automata with a counter whose value can range over non-negative integers and be tested for zero. The updates and tests applicable to the counter can further be made parametric by introducing a set of integer-valued variables called parameters. The LTL parameter synthesis problem for such automata asks whether a valuation of the parameters exists such that all infinite runs of the automaton satisfy an LTL specification. Building upon the existing works in the literature, (i) we show a careful re-encoding of the problem into a decidable restriction of Presburger Arithmetic with Divisibility (PAD), the largest known decidable fragment of PAD till now; (ii) We prove that the parameter synthesis problem is decidable in general and in 3NEXP; (iii) We give EXPSPACE algorithms for the special cases of the problem where parameters can only be used in counter tests. Finally, (iv) we briefly present the decidability result of this problem on an extension of this model with Parikh constraints
Apprentissage et vérification de systèmes complexes avec des spécifications temporelles
No full textIn the past decade, there has been an unprecedented rise in the incorporation of complex cyber-physical systems being used in performing complex tasks. Verification of these systems is necessary to ensure the safety and reliability of these systems, especially in safety-critical scenarios. Formal verification has been proven to be a time-tested method to systematically verify these systems. In particular, it provides techniques for monitoring system executions against a formal specification. Often, these specifications are hard to design manually, necessitating a need to automatically generate them from system executions to be used for verification purposes. Temporal logic has gained popularity as a formal specification due to its mathematical rigour, human interpretability, and compatibility with various formal verification techniques. The objective of this thesis is twofold: (i) Develop algorithms to automatically learn temporal specifications from system executions; (ii) Apply formal verification techniques to assess the correctness of the system against the acquired specifications.To achieve these objectives, in the learning part, we present two algorithms to learn specifications in temporal logics such as LTL, MTL and STL. Our algorithms are in emph{passive learning} setting that learn specifications that separate a finite set of positive system behaviours from a finite set of negative ones. For LTL specifications, we present a dynamic programming based algorithm that leverages a normal form for a fragment of LTL and uses efficient enumeration techniques to learn concise formulas from system executions. For MTL and STL, we develop SMT-solver based techniques to learn formulas that are not only concise but also efficient to be applied for formal verification of the system. Our algorithms are implemented in tools called SCARLET and TEAL, and their efficiency is demonstrated through experimental results. For the verification part, we focus on the LTL parameter-synthesis problems of one-counter automata, which is one of the fundamental formal models to represent complex systems, namely systems with discrete yet infinite state space. One-counter automata are obtained by extending classical finite-state automata with a counter whose value can range over non-negative integers and be tested for zero. The updates and tests applicable to the counter can further be made parametric by introducing a set of integer-valued variables called parameters. The LTL parameter synthesis problem for such automata asks whether a valuation of the parameters exists such that all infinite runs of the automaton satisfy an LTL specification. Building upon the existing works in the literature, (i) we show a careful re-encoding of the problem into a decidable restriction of Presburger Arithmetic with Divisibility (PAD), the largest known decidable fragment of PAD till now; (ii) We prove that the parameter synthesis problem is decidable in general and in 3NEXP; (iii) We give EXPSPACE algorithms for the special cases of the problem where parameters can only be used in counter tests. Finally, (iv) we briefly present the decidability result of this problem on an extension of this model with Parikh constraints.Au cours de la dernière décennie, on a assisté à une augmentation sans précédent de l'incorporation de systèmes cyber-physiques complexes utilisés pour effectuer des tâches complexes. La vérification de ces systèmes est nécessaire pour garantir leur sécurité et leur fiabilité, en particulier dans les scénarios de sécurité critiques. La vérification formelle s'est avérée être une méthode éprouvée pour vérifier systématiquement ces systèmes. Elle fournit notamment des techniques permettant de contrôler l'exécution des systèmes par rapport à une spécification formelle. Souvent, ces spécifications sont difficiles à concevoir manuellement, d'où la nécessité de les générer automatiquement à partir des exécutions du système pour les utiliser à des fins de vérification. La logique temporelle a gagné en popularité en tant que spécification formelle en raison de sa rigueur mathématique, de son interprétabilité par l'homme et de sa compatibilité avec diverses techniques de vérification formelle. L'objectif de cette thèse est double : (i) Développer des algorithmes pour apprendre automatiquement des spécifications temporelles à partir d'exécutions de systèmes ; (ii) Appliquer des techniques de vérification formelle pour évaluer l'exactitude du système par rapport aux spécifications acquises.Pour atteindre ces objectifs, dans la partie apprentissage, nous présentons deux algorithmes pour apprendre des spécifications dans des logiques temporelles telles que LTL, MTL et STL. Nos algorithmes sont dans le cadre de l'apprentissage passif et apprennent des spécifications qui séparent un ensemble fini de comportements positifs du système d'un ensemble fini de comportements négatifs. Pour les spécifications LTL, nous présentons un algorithme basé sur la programmation dynamique qui s'appuie sur une forme normale pour un fragment de LTL et utilise des techniques d'énumération efficaces pour apprendre des formules concises à partir des exécutions du système. Pour MTL et STL, nous développons des techniques basées sur un résolveur SMT pour apprendre des formules qui sont non seulement concises mais aussi efficaces pour être appliquées à la vérification formelle du système. Nos algorithmes sont mis en œuvre dans des outils appelés SCARLET et TEAL, et leur efficacité est démontrée par des résultats expérimentaux. Pour la partie vérification, nous nous concentrons sur les problèmes de synthèse de paramètres LTL des One-counter automata, qui est l'un des modèles formels fondamentaux pour représenter les systèmes complexes, à savoir les systèmes avec un espace d'état discret mais infini. One-counter automata sont obtenus en étendant les automates classiques à états finis avec un compteur dont la valeur peut s'étendre sur des entiers non négatifs et être testée pour zéro. Les mises à jour et les tests applicables au compteur peuvent être paramétrés en introduisant un ensemble de variables à valeur entière appelées paramètres. Le problème de la synthèse des paramètres LTL pour de tels automates est de savoir s'il existe une évaluation des paramètres telle que toutes les exécutions infinies de l'automate satisfont une spécification LTL. En s'appuyant sur les travaux existants dans la littérature, (i) nous montrons un réencodage prudent du problème en une restriction décidable de l'arithmétique de Presburger avec divisibilité (PAD), le plus grand fragment décidable connu de PAD jusqu'à présent ; (ii) Nous prouvons que le problème de la synthèse des paramètres est décidable en général et en 3NEXP ; (iii) Nous donnons des algorithmes EXPSPACE pour les cas particuliers du problème où les paramètres ne peuvent être utilisés que dans des contre-tests. Enfin, (iv) nous présentons brièvement le résultat de décidabilité de ce problème sur une extension de ce modèle avec des contraintes de Parikh
Learning and verifying temporal specifications for cyber-physical systems
No full textAbstract: In the past decade, there has been an unprecedented rise in the incorporation of cyber-physical systems used to perform complex tasks. Verifying these systems is necessary to ensure their safety and reliability, especially in safety-critical scenarios. Formal verification has been proven to be a time-tested method to systematically verify these systems. In particular, it provides techniques for monitoring system executions against a formal specification. Temporal logic has gained popularity as a formal specification due to its mathematical rigour, human interpretability, and compatibility with various formal verification techniques. But, often, these specifications are hard to design manually, necessitating a need to automatically generate them from system executions. The objective of this thesis is twofold: (i) Develop algorithms to automatically learn temporal specifications from system executions; (ii) Apply formal verification techniques to assess the correctness of the system against the acquired specifications. To achieve these objectives, in the learning part, we present two algorithms to learn specifications in temporal logics such as LTL, MTL, and STL. We present a dynamic programming-based algorithm for LTL specifications that leverages a normal form for a fragment of LTL and uses efficient enumeration techniques to learn concise formulas from system executions. For MTL and STL, we develop SMT-solver-based techniques to learn formulas that are not only concise but also efficient to be applied for formal verification of the system. Our algorithms are implemented in tools called SCARLET and TEAL, and their efficiency is demonstrated through experimental results. In the verification part, we focus on the LTL parameter-synthesis problems of one-counter automata, one of the fundamental formal models to represent complex systems, namely systems with discrete yet infinite state space. One-counter automata are obtained by extending classical finite-state automata with a counter whose value can range over non-negative integers and be tested for zero. The updates and tests can be further made parametric by introducing a set of integer-valued variables called parameters. The LTL parameter-synthesis problem asks whether a valuation of the parameters exists such that all runs of the automaton satisfy an LTL specification. In this work, we show that (i) this problem is encodable into a decidable restriction of Presburger Arithmetic with Divisibility (PAD), (ii) the parameter synthesis problem is decidable, and in 3NEXP; (iii) the problem is in EXPSPACE where parameters can only be used in counter tests
Apprentissage et vérification de systèmes complexes avec des spécifications temporelles
No full textIn the past decade, there has been an unprecedented rise in the incorporation of complex cyber-physical systems being used in performing complex tasks. Verification of these systems is necessary to ensure the safety and reliability of these systems, especially in safety-critical scenarios. Formal verification has been proven to be a time-tested method to systematically verify these systems. In particular, it provides techniques for monitoring system executions against a formal specification. Often, these specifications are hard to design manually, necessitating a need to automatically generate them from system executions to be used for verification purposes. Temporal logic has gained popularity as a formal specification due to its mathematical rigour, human interpretability, and compatibility with various formal verification techniques. The objective of this thesis is twofold: (i) Develop algorithms to automatically learn temporal specifications from system executions; (ii) Apply formal verification techniques to assess the correctness of the system against the acquired specifications.To achieve these objectives, in the learning part, we present two algorithms to learn specifications in temporal logics such as LTL, MTL and STL. Our algorithms are in emph{passive learning} setting that learn specifications that separate a finite set of positive system behaviours from a finite set of negative ones. For LTL specifications, we present a dynamic programming based algorithm that leverages a normal form for a fragment of LTL and uses efficient enumeration techniques to learn concise formulas from system executions. For MTL and STL, we develop SMT-solver based techniques to learn formulas that are not only concise but also efficient to be applied for formal verification of the system. Our algorithms are implemented in tools called SCARLET and TEAL, and their efficiency is demonstrated through experimental results. For the verification part, we focus on the LTL parameter-synthesis problems of one-counter automata, which is one of the fundamental formal models to represent complex systems, namely systems with discrete yet infinite state space. One-counter automata are obtained by extending classical finite-state automata with a counter whose value can range over non-negative integers and be tested for zero. The updates and tests applicable to the counter can further be made parametric by introducing a set of integer-valued variables called parameters. The LTL parameter synthesis problem for such automata asks whether a valuation of the parameters exists such that all infinite runs of the automaton satisfy an LTL specification. Building upon the existing works in the literature, (i) we show a careful re-encoding of the problem into a decidable restriction of Presburger Arithmetic with Divisibility (PAD), the largest known decidable fragment of PAD till now; (ii) We prove that the parameter synthesis problem is decidable in general and in 3NEXP; (iii) We give EXPSPACE algorithms for the special cases of the problem where parameters can only be used in counter tests. Finally, (iv) we briefly present the decidability result of this problem on an extension of this model with Parikh constraints.Au cours de la dernière décennie, on a assisté à une augmentation sans précédent de l'incorporation de systèmes cyber-physiques complexes utilisés pour effectuer des tâches complexes. La vérification de ces systèmes est nécessaire pour garantir leur sécurité et leur fiabilité, en particulier dans les scénarios de sécurité critiques. La vérification formelle s'est avérée être une méthode éprouvée pour vérifier systématiquement ces systèmes. Elle fournit notamment des techniques permettant de contrôler l'exécution des systèmes par rapport à une spécification formelle. Souvent, ces spécifications sont difficiles à concevoir manuellement, d'où la nécessité de les générer automatiquement à partir des exécutions du système pour les utiliser à des fins de vérification. La logique temporelle a gagné en popularité en tant que spécification formelle en raison de sa rigueur mathématique, de son interprétabilité par l'homme et de sa compatibilité avec diverses techniques de vérification formelle. L'objectif de cette thèse est double : (i) Développer des algorithmes pour apprendre automatiquement des spécifications temporelles à partir d'exécutions de systèmes ; (ii) Appliquer des techniques de vérification formelle pour évaluer l'exactitude du système par rapport aux spécifications acquises.Pour atteindre ces objectifs, dans la partie apprentissage, nous présentons deux algorithmes pour apprendre des spécifications dans des logiques temporelles telles que LTL, MTL et STL. Nos algorithmes sont dans le cadre de l'apprentissage passif et apprennent des spécifications qui séparent un ensemble fini de comportements positifs du système d'un ensemble fini de comportements négatifs. Pour les spécifications LTL, nous présentons un algorithme basé sur la programmation dynamique qui s'appuie sur une forme normale pour un fragment de LTL et utilise des techniques d'énumération efficaces pour apprendre des formules concises à partir des exécutions du système. Pour MTL et STL, nous développons des techniques basées sur un résolveur SMT pour apprendre des formules qui sont non seulement concises mais aussi efficaces pour être appliquées à la vérification formelle du système. Nos algorithmes sont mis en œuvre dans des outils appelés SCARLET et TEAL, et leur efficacité est démontrée par des résultats expérimentaux. Pour la partie vérification, nous nous concentrons sur les problèmes de synthèse de paramètres LTL des One-counter automata, qui est l'un des modèles formels fondamentaux pour représenter les systèmes complexes, à savoir les systèmes avec un espace d'état discret mais infini. One-counter automata sont obtenus en étendant les automates classiques à états finis avec un compteur dont la valeur peut s'étendre sur des entiers non négatifs et être testée pour zéro. Les mises à jour et les tests applicables au compteur peuvent être paramétrés en introduisant un ensemble de variables à valeur entière appelées paramètres. Le problème de la synthèse des paramètres LTL pour de tels automates est de savoir s'il existe une évaluation des paramètres telle que toutes les exécutions infinies de l'automate satisfont une spécification LTL. En s'appuyant sur les travaux existants dans la littérature, (i) nous montrons un réencodage prudent du problème en une restriction décidable de l'arithmétique de Presburger avec divisibilité (PAD), le plus grand fragment décidable connu de PAD jusqu'à présent ; (ii) Nous prouvons que le problème de la synthèse des paramètres est décidable en général et en 3NEXP ; (iii) Nous donnons des algorithmes EXPSPACE pour les cas particuliers du problème où les paramètres ne peuvent être utilisés que dans des contre-tests. Enfin, (iv) nous présentons brièvement le résultat de décidabilité de ce problème sur une extension de ce modèle avec des contraintes de Parikh
Going Beyond Counting First Authors in Author Co-citation Analysis
Get PDFThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
Variations on the Author
Get PDF“Variations on the Author” discusses two of Eduardo Coutinho’s recent films (Um Dia na Vida, from 2010, and Últimas Conversas, posthumously released in 2015) and their contribution to the general question of documentary authorship. The director’s filmography is characterized by a consistent yet self-effacing form of authorial self-inscription: Coutinho often features as an interviewer that rather than express opinions propels discourses; an interviewer that is good at listening. This mode of self-inscription characterizes him as an author who is not expressive but who is nonetheless markedly present on the screen. In Um Dia na Vida, however, Coutinho is completely absent form the image, while Últimas Conversas, on the contrary, includes a confessional prologue that moves the director from the margins to the center of his films. This article examines the ways in which these works stand out in the filmography of a director who offers new insights into the notion of cinematic authorship
Appropriate Similarity Measures for Author Cocitation Analysis
Get PDFWe provide a number of new insights into the methodological discussion about author cocitation analysis. We first argue that the use of the Pearson correlation for measuring the similarity between authors’ cocitation profiles is not very satisfactory. We then discuss what kind of similarity measures may be used as an alternative to the Pearson correlation. We consider three similarity measures in particular. One is the well-known cosine. The other two similarity measures have not been used before in the bibliometric literature. Finally, we show by means of an example that our findings have a high practical relevance.information science;Pearson correlation;cosine;similarity measure;author cocitation analysis
Dispelling the Myths Behind First-author Citation Counts
Get PDFWe conducted a full-scale evaluative citation analysis study of scholars in the XML research field to explore just how different from each other author rankings resulting from different citation counting methods actually are, and to demonstrate the capability of emerging data and tools on the Web in supporting more realistic citation counting methods. Our results contest some common arguments for the continued
use of first-author citation counts in the evaluation of scholars, such as high correlations between author rankings by first-author citation counts and other citation
counting methods, and high costs of using more realistic citation counting methods that are not well-supported by the ISI databases. It is argued that increasingly available digital full text research papers make it possible for citation analysis studies to go beyond what the ISI databases have directly supported and to employ more
sophisticated methods
- …
