1,721,036 research outputs found
Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2014, Verona, Italy, September 10-12, 2014
No full text
A Model Checking Procedure for Interval Temporal Logics based on Track Representatives
Full text linkModel checking is commonly recognized as one of the most effective tools for system verification. While it has been systematically investigated in the context of classical, point-based temporal logics, it is still largely unexplored in the interval logic setting. Recently, a non-elementary model checking algorithm for Halpern and Shoham’s modal logic of time intervals HS, interpreted over finite Kripke structures, has been proposed, together with a proof of the EXPSPACE-hardness of the problem. In this paper, we devise an EXPSPACE model checking procedure for two meaningful HS fragments. It exploits a suitable contraction technique that allows one to replace sufficiently long tracks of a Kripke structure by equivalent shorter ones
Taming Strategy Logic: Non-Recurrent Fragments
Full text linkStrategy Logic (SL for short) is one of the prominent languages for reasoning about the strategic abilities of agents in a multi-agent setting. This logic extends LTL with first-order quantifiers over the agent strategies and encompasses other formalisms, such as ATL* and CTL*. The model-checking problem for SL and several of its fragments have been extensively studied. On the other hand, the picture is much less clear on the satisfiability front, where the problem is undecidable for the full logic. In this work, we study two fragments of One-Goal SL, where the nesting of sentences within temporal operators is constrained. We show that the satisfiability problem for these logics, and for the corresponding fragments of ATL* and CTL*, is ExpSpace and PSpace-Complete, respectively
Complexity of timeline-based planning over dense temporal domains: Exploring the middle ground
Full text linkIn this paper, we address complexity issues for timeline-based planning over dense temporal domains. The planning problem is modeled by means of a set of independent, but interacting, components, each one represented by a number of state variables, whose behavior over time (timelines) is governed by a set of temporal constraints (synchronization rules). While the temporal domain is usually assumed to be discrete, here we consider the dense case. Dense timeline-based planning has been recently shown to be undecidable in the general case; decidability (NP-completeness) can be recovered by restricting to purely existential synchronization rules (trigger-less rules). In this paper, we investigate the unexplored area of intermediate cases in between these two extremes. We first show that decidability and non-primitive recursive hardness can be proved by admitting synchronization rules with a trigger, but forcing them to suitably check constraints only in the future with respect to the trigger (future simple rules). More "tractable" results can be obtained by additionally constraining the form of intervals in future simple rules: EXPSPACE-completeness is guaranteed by avoiding singular intervals, PSPACE-completeness by admitting only intervals of the forms [0, a] and [b, +∞[
Web and Wireless Geographical Information Systems11th International Symposium, W2GIS 2012, Naples, Italy, April 12-13, 2012. Proceedings.
No full textThis volume contains the papers selected for presentation at the 11th edition of the International Symposium on Web and Wireless Geographical Information Systems (W2GIS 2012), hosted by the University of Naples “Federico II” in the dazzling city of Naples, Italy, in April 2012.
W2GIS is a series of events alternating between Europe and East Asia. It aims at providing a forum for discussing advances in theoretical, technical, and practical issues in the field of wireless and Internet technologies suited for the spreading, usage, and processing of geo-referenced data. W2GIS now represents a prestigious event within the research community that continues to develop and expand.
For the 2012 edition, we received 32 submissions from 12 countries in 4 continents. Each paper received three reviews and based on these reviews, 13 full papers and 4 short papers were selected for presentation at the symposium and inclusion in Springer LNCS Volume 7236. The accepted papers are all of excellent quality and cover topics that range from mobile GIS and location-based services to spatial information retrieval and wireless sensor networks.
We had the privilege of having a distinguished invited talk by Christopher B. Jones from the School of Computer Science at Cardiff University (UK). The best paper of the symposium was selected by the Steering Committee and invited to submit an extended version for publication in the Journal of Spatial Information Science.
We wish to thank all authors that contributed to this symposium for the high quality of their papers and presentations. Our sincere thanks go to Springer’s LNCS team. We would also like to acknowledge and thank the Program Committee members for the quality and timeliness of their reviews. Finally, many thanks to Christophe Claramunt, Michela Bertolotto, and the entire Steering Committee members for providing continuous support and advice
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
Pspace-Completeness of the Temporal Logic of Sub-Intervals and Suffixes
Full text linkIn this paper, we establish Pspace-completeness of the finite satisfiability and model checking problems for the fragment of Halpern and Shoham interval logic with modality ⟨E⟩, for the "suffix" relation on pairs of intervals, and modality ⟨D⟩, for the "sub-interval" relation, under the homogeneity assumption. The result significantly improves the Expspace upper bound recently established for the same fragment, and proves the rather surprising fact that the complexity of the considered problems does not change when we add either the modality for suffixes (⟨E⟩) or, symmetrically, the modality for prefixes (⟨B⟩) to the logic of sub-intervals (featuring only ⟨D⟩)
Automata-Theoretic Characterisations of Branching-Time Temporal Logics
Full text linkCharacterisations theorems serve as important tools in model theory and can be used to assess and compare the expressive power of temporal languages used for the specification and verification of properties in formal methods. While complete connections have been established for the linear-time case between temporal logics, predicate logics, algebraic models, and automata, the situation in the branching-time case remains considerably more fragmented. In this work, we provide an automata-theoretic characterisation of some important branching-time temporal logics, namely CTL* and ECTL* interpreted on arbitrary-branching trees, by identifying two variants of Hesitant Tree Automata that are proved equivalent to those logics. The characterisations also apply to Monadic Path Logic and the bisimulation-invariant fragment of Monadic Chain Logic, again interpreted over trees. These results widen the characterisation landscape of the branching-time case and solve a forty-year-old open question
- …
