1,721,024 research outputs found
Constraining Cycle Alternations in Model Checking for Interval Temporal Logic
Full text linkModel checking is one of the most successful techniques in system verification. While a variety of methods and tools exist to check properties expressed in point-based temporal logics, like LTL and CTL, model checking for interval temporal logic has entered the research agenda only very recently. In previous work, we devised a non-elementary model checking procedure for Halpern and Shoham's modal logic of time intervals, interpreted over finite Kripke structures, and an EXPSPACE algorithm for two meaningful fragments of it. In this paper, we show that the latter algorithm can be suitably tailored in order to check a subset of the computations of a system, that satisfy a given bound on the number of cycle alternations, by making use of a polynomial (instead of exponential) working space. We also prove that such a revised algorithm turns out to be complete for Kripke structures whose strongly connected components are simple cycle
Model Checking: il Metodo Intervallare
Full text linkI metodi formali sono metodologie strutturate che supportano lo sviluppo di sistemi critici allo scopo di dimostrare la loro correttezza con rigore matematico, fornendo tecniche e strumenti di verifica efficaci, e riducendo il tempo del processo di verifica, aumentando contemporaneamente il grado di copertura.
Il model checking (MC) è una famiglia di metodi formali che sono stati accettati dal mondo dell’industria e stanno diventando parte integrante di standard. Nel MC, alcune proprietà di un sistema di transizione vengono espresse mediante linguaggi di specifica e, successivamente, queste sono verificate su un modello del sistema stesso (di solito una struttura di Kripke), tramite l’enumerazione completa degli stati raggiungibili. Tale tecnica è automatica ed ogni volta che è violata una proprietà desiderata, viene fornito un controesempio che illustra un comportamento che falsifica la proprietà: ciò è utile per il debugging.
Le più famose tecniche di MC furono sviluppate negli anni 80 considerando le famose logiche temporali LTL e CTL, che sono basate su punti. Tuttavia, esistono alcune proprietà che potremmo voler verificare che hanno inerentemente una semantica intervallare e quindi non possono essere espresse da logiche puntuali, per esempio: “la proposizione p deve valere in almeno un dato numero medio di stati del sistema, in un settore di computazione specifico”. Le logiche temporali intervallari entrano in gioco in questi casi, permettendoci di ragionare su aspetti temporali in modo diverso: esse adottano gli intervalli, invece dei punti, come loro entità primitive. Questa caratteristica dà loro l’abilità di esprimere proprietà intervallari, come azioni con durata e aggregazioni temporali, che non possono essere trattate nelle logiche puntuali.
La logica modale degli intervalli temporali di Halpern e Shoham (HS) è una delle più famose logiche intervallari: essa ha una modalità per ognuna delle 13 relazioni di ordinamento fra coppie di intervalli, eccetto l’uguaglianza. In questa tesi viene considerato il problema del MC basato su HS, come linguaggio di specifica delle proprietà, il quale ha ricevuto poca attenzione in letteratura. L’idea è quella di valutare formule di HS su strutture di Kripke finite, per riuscire a verificare la correttezza di un sistema rispetto a proprietà intervallari. A questo scopo, ognuno dei percorsi finiti di una struttura di Kripke (i quali possono essere presenti in quantità infinita) è interpretato come un intervallo, e le proprietà atomiche che valgono su quest’ultimo sono definite sulla base di quelle degli stati che lo costituiscono, inizialmente secondo il principio di omogeneità: esso prevede che una proprietà atomica valga su un intervallo se e solo se vale su tutti i suoi sottointervalli. Dimostriamo che il MC per HS su strutture di Kripke finite è decidibile (la sua complessità ha un upper bound non-elementare); poi mostriamo che è EXPSPACE-hard.
Poiché il problema non ammette procedure di decisione polinomiali, consideriamo anche frammenti di HS, i quali hanno complessità migliori—da EXPSPACE, giù fino a livelli bassi della gerarchia polinomiale—pur tuttavia mantenendo l’abilità di esprimere proprietà intervallari significative. Presentiamo svariati algoritmi di MC, costruiti ad-hoc per gli specifici frammenti considerati, e fondati su concetti e tecniche diversi fra loro.
Studiamo poi il potere espressivo di HS in confronto a quello delle logiche puntuali LTL, CTL e CTL∗, sempre sotto l’ipotesi di omogeneità, la quale viene poi rilassata mostrando quali sono le implicazioni sul MC per HS ed i suoi frammenti, e sull’espressività della logica stessa.
Infine, consideriamo una possibile alternativa alle strutture di Kripke: studiamo un modello di sistemi più espressivo, che ci permette di descrivere gli stessi in termini delle loro proprietà intervallari.
Ciò apre la strada a un MC intervallare più generale.Formal methods are structured methodologies that support the development of critical systems, with the aim of establishing system correctness with mathematical rigor, providing effective verification techniques and tools, and reducing verification time while simultaneously increasing coverage.
Model checking (MC) is a family of formal methods that have been accepted by industry and are becoming integral part of standards. In MC, some properties of a transition system are expressed in suitable specification languages and then verified over a model of the system itself (usually a Kripke structure) through exhaustive enumeration of the reachable states. This technique is fully automatic and every time the design violates a desired property, a counterexample is produced, which illustrates a behavior falsifying such a property: this is extremely useful for debugging.
The most famous MC techniques were developed from the late 80s, bearing in mind the well-known “point-based” temporal logics LTL and CTL. However, while the expressiveness of such logics is beyond doubt, there are some properties we may want to check that are inherently “interval-based” and thus cannot be expressed by point-based temporal logics, e.g., “the proposition p has to hold in at least an average number of system states in a given computation sector”. Here interval temporal logics (ITLs) come into play, providing an alternative setting for reasoning about time. Such logics deal with intervals, instead of points, as their primitive entities: this feature gives them the ability of expressing temporal properties, such as actions with duration, accomplishments, and temporal aggregations, which cannot be dealt with in standard point-based logics.
The Halpern and Shoham’s modal logic of time intervals (HS, for short) is one of the most famous ITLs: it features one modality for each of the 13 possible ordering relations between pairs of intervals, apart from equality. In this thesis we focus our attention on MC based on HS, in the role of property specification language, for which a little work has been done if compared to MC for point-based temporal logics. The idea is to evaluate HS formulas on finite Kripke structures, making it possible to check the correctness of the behavior of systems with respect to meaningful interval properties. To this end, we interpret each one of the (possibly infinitely many) finite paths of a Kripke structure as an interval, and we define its atomic properties on the basis of the properties of the states composing it, at first assuming the homogeneity principle: the latter enforces an atomic property to hold over an interval if and only if it holds over all its subintervals. We prove that MC for HS interpreted over finite Kripke structures is a decidable problem (whose computational complexity has a nonelementary upper bound), and then we show it to be EXPSPACE-hard.
Since the problem provably admits no polynomial-time decision procedure, we also focus on HS fragments, which feature considerably better complexities—from EXPSPACE, down to low levels of the polynomial hierarchy—yet retaining the ability to capture meaningful interval properties of state transition systems. Several MC algorithms are presented, tailored to the specific fragments being considered, and founded on concepts and techniques different from each other.
Moreover, we study the expressive power of HS in MC, in comparison with that of the standard point-based logics LTL, CTL and CTL∗, still under the homogeneity principle, which is then relaxed showing how this impacts on the complexity of MC for HS and its fragments, and on the expressiveness of the logic.
Finally, we consider a possible replacement of Kripke structures by a more expressive model, which allows us to directly describe systems in terms of their interval-based behavior and properties, thus paving the way for a more general interval-based MC
I monumenti agli eroi dello sport in Emilia-Romagna. I casi di Dorando Pietri, Ayrton Senna e Marco Pantani
No full textL’articolo propone una riflessione sui monumenti dedicati ai campioni dello sport a partire da tre casi emiliano-romagnoli: la statua dedicata a Dorando Pietri a Carpi; le installazioni in memoria di Marco Pantani a Cesenatico e a Imola; e il memoriale che ricorda Ayrton Senna realizzato nell’autodromo di Imola. Nonostante le differenti caratteristiche e finalità, i lavori sono accomunati dalla dimensione eroica degli atleti rappresentati, alimentata anche dalla tragicità delle loro vicende, e rimandano tutti al tema della memoria nella dimensione sportiva
Model Checking for Fragments of the Interval Temporal Logic HS at the Low Levels of the Polynomial Time Hierarchy
Full text linkSome temporal properties of reactive systems, such as actions with duration and temporal aggregations, which are inherently interval-based, can not be properly expressed by the standard, point-based temporal logics LTL, CTL and CTL⁎, as they give a state-by-state account of system evolution. Conversely, interval temporal logics—which feature intervals, instead of points, as their primitive entities—naturally express them.
We study the model checking (MC) problem for Halpern and Shoham's modal logic of time intervals (HS), interpreted on Kripke structures, under the homogeneity assumption. HS is the best known interval-based temporal logic, which has one modality for each of the 13 ordering relations between pairs of intervals (Allen's relations), apart from equality. We focus on MC for some HS fragments featuring modalities for (a subset of) Allen's relations meet, met-by, started-by, and finished-by, showing that it is in
P^NP. Additionally, we provide some complexity lower bounds to the problem
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe 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
Full text link“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
Full text linkWe 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
Model checking for fragments of Halpern and Shoham's interval temporal logic based on track representatives
Full text linkModel checking allows one to automatically verify a specification of the expected properties of a system against a formal model of its behavior (generally, a Kripke structure). Point-based temporal logics, such as LTL, CTL, and CTL⁎, that describe how the system evolves state-by-state, are commonly used as specification languages. They proved themselves quite successful in a variety of application domains. However, properties constraining the temporal ordering of temporally extended events as well as properties involving temporal aggregations, which are inherently interval-based, can not be properly dealt with by them. Interval temporal logics (ITLs), that take intervals as their primitive temporal entities, turn out to be well-suited for the specification and verification of interval properties of computations (we interpret all the tracks of a Kripke structure as computation intervals). In this paper, we study the model checking problem for some fragments of Halpern and Shoham's modal logic of time intervals (HS). HS features one modality for each possible ordering relation between pairs of intervals (the so-called Allen's relations). First, we describe an EXPSPACE model checking algorithm for the HS fragment of Allen's relations meets, met-by, starts, started-by, and finishes, which exploits the possibility of finding, for each track (of unbounded length), an equivalent bounded-length track representative. While checking a property, it only needs to consider tracks whose length does not exceed the given bound. Then, we prove the model checking problem for such a fragment to be PSPACE-hard. Finally, we identify other well-behaved HS fragments which are expressive enough to capture meaningful interval properties of systems, such as mutual exclusion, state reachability, and non-starvation, and whose computational complexity is less than or equal to that of LTL. © 2017 Elsevier Inc
- …
