| 1. |
- Aceto, Luca, et al.
(författare)
-
A complete classification of the expressiveness of interval logics of Allen’s relations : the general and the dense cases
- 2016
-
Ingår i: Acta Informatica. - : Springer Science and Business Media LLC. - 0001-5903 .- 1432-0525. ; 53:3, s. 207-246
-
Tidskriftsartikel (refereegranskat)abstract
- Interval temporal logics take time intervals, instead of time points, as their primitive temporal entities. One of the most studied interval temporal logics is Halpern and Shoham’s modal logic of time intervals HS, which associates a modal operator with each binary relation between intervals over a linear order (the so-called Allen’s interval relations). In this paper, we compare and classify the expressiveness of all fragments of HS on the class of all linear orders and on the subclass of all dense linear orders. For each of these classes, we identify a complete set of definabilities between HS modalities, valid in that class, thus obtaining a complete classification of the family of all 4096 fragments of HS with respect to their expressiveness. We show that on the class of all linear orders there are exactly 1347 expressively different fragments of HS, while on the class of dense linear orders there are exactly 966 such expressively different fragments.
|
|
| 2. |
- Bulling, Nils, et al.
(författare)
-
Logics for reasoning about strategic abilities in multi-player games
- 2015
-
Ingår i: Models of strategic reasoning. - Berlin : Springer. - 9783662485408 ; , s. 93-136
-
Bokkapitel (refereegranskat)abstract
- We introduce and discuss basic concepts, ideas, and logical formalisms used for reasoning about strategic abilities in multi-player games. In particular, we present concurrent game models and the alternating time temporal logic ATL∗ and its fragment ATL. We discuss variations of the language and semantics of ATL∗ that take into account the limitations and complications arising from incomplete information, perfect or imperfect memory of players, reasoning within dynamically changing strategy contexts, or using stronger, constructive concepts of strategy. Finally, we briefly summarize some technical results regarding decision problems for some variants of ATL.
|
|
| 3. |
- Cerrito, Serenella, et al.
(författare)
-
Minimisation of Models Satisfying CTL Formulas
- 2019
-
Ingår i: 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). - 9783959771276 ; , s. 13:1-13:15
-
Konferensbidrag (refereegranskat)abstract
- We study the problem of minimisation of a given finite pointed Kripke model satisfying a given CTL formula, with the only objective to preserve the satisfaction of that formula in the resulting reduced model. We consider minimisations of the model with respect both to state-based redundancies and formula-based redundancies in that model. We develop a procedure computing all such minimisations, illustrate it with some examples, and provide some complexity analysis for it.
|
|
| 4. |
- Cerrito, Serenella, et al.
(författare)
-
Optimal Tableaux Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-time Temoral Logic ATL
- 2015
-
Ingår i: ACM Transactions on Computational Logic. - : Association for Computing Machinery (ACM). - 1529-3785 .- 1557-945X. ; 17:1
-
Tidskriftsartikel (refereegranskat)abstract
- We develop a sound, complete, and practically implementable tableau-based decision method for constructive satisfiability testing and model synthesis for the fragment ATL+ of the full alternating-time temporal logic ALT*. The method extends in an essential way a previously developed tableau-based decision method for ATL and works in 2EXPTIME, which is the optimal worst-case complexity of the satisfiability problem for ATL+. We also discuss how suitable parameterizations and syntactic restrictions on the class of input ATL+formulas can reduce the complexity of the satisfiability problem.
|
|
| 5. |
-
Computer Science Logic 2017
- 2017
-
Proceedings (redaktörskap) (refereegranskat)abstract
- Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). It is an interdisciplinary conference, spanning across both basic and application oriented research in mathematical logic and computer science. CSL started as a series of international workshops on Computer Science Logic, and became at its sixth meeting the Annual Conference of the EACSL.The 26th annual EACSL conference Computer Science Logic (CSL 2017) was held in Stockholm from August 20 to August 24, 2017. CSL 2017 was organised jointly by members of the Departments of Philosophy and of Mathematics and Stockholm University, and of the Department of Theoretical Computer Science at KTH Royal Institute of Technology.
|
|
| 6. |
- Condurache, Rodica, et al.
(författare)
-
Dynamic Multi-Agent Systems : Conceptual Framework, Automata-Based Modelling and Verification
- 2019
-
Ingår i: PRIMA 2019: Principles and Practice of Multi-Agent Systems. - Cham : Springer. - 9783030337919 - 9783030337926 ; , s. 106-122
-
Konferensbidrag (refereegranskat)abstract
- We study dynamic multi-agent systems (dmass). These are multi-agent systems with explicitly dynamic features, where agents can join and leave the system during the evolution. We propose a general conceptual framework for modelling such dmass and argue that it can adequately capture a variety of important and representative cases. We then present a concrete modelling framework for a large class of dmass, composed in a modular way from agents specified by means of automata-based representations. We develop generic algorithms implementing the dynamic behaviour, namely addition and removal of agents in such systems. Lastly, we state and discuss several formal verification tasks that are specific for dmass and propose general algorithmic solutions for the class of automata representable dmass.
|
|
| 7. |
- Conradie, Willem, et al.
(författare)
-
Algorithmic Correspondence for Relevance Logics I. The Algorithm PEARL
- 2022
-
Ingår i: Alasdair Urquhart on Nonclassical and Algebraic Logic and Complexity of Proofs. - Cham : Springer. - 9783030714291 - 9783030714307 ; , s. 163-211
-
Bokkapitel (refereegranskat)abstract
- We apply and extend the theory and methods of algorithmic correspondence theory for modal logics, developed over the past 20 years, to the language LR of relevance logics with respect to their standard Routley–Meyer relational semantics. We develop the non-deterministic algorithmic procedure PEARLPEARL for computing first-order equivalents of formulae of the language LR, in terms of that semantics. PEARLPEARL is an adaptation of the previously developed algorithmic procedures SQEMA (for normal modal logics) and ALBA (for distributive and non-distributive modal logics). We then identify a large syntactically defined class of inductive formulae in LR, analogous to previously defined such classes in the classical, distributive and non-distributive modal logic settings, and show that PEARLPEARL succeeds for every inductive formula and correctly computes a first-order definable condition which is equivalent to it with respect to frame validity. We also provide a detailed comparison with two earlier works, each extending the class of Sahlqvist formulae to relevance logics, and show that both are subsumed by simple subclasses of inductive formulae.
|
|
| 8. |
- Conradie, Willem, et al.
(författare)
-
Logic and Discrete Mathematics : a Concise Introduction
- 2015
-
Bok (refereegranskat)abstract
- This book features a unique combination of comprehensive coverage of logic with a solid exposition of the most important fields of discrete mathematics, presenting material that has been tested and refined by the authors in university courses taught over more than a decade. The chapters on logic - propositional and first-order - provide a robust toolkit for logical reasoning, emphasizing the conceptual understanding of the language and the semantics of classical logic as well as practical applications through the easy to understand and use deductive systems of Semantic Tableaux and Resolution. The chapters on set theory, number theory, combinatorics and graph theory combine the necessary minimum of theory with numerous examples and selected applications. Written in a clear and reader-friendly style, each section ends with an extensive set of exercises, most of them provided with complete solutions which are available in the accompanying solutions manual.
|
|
| 9. |
|
|
| 10. |
- Demri, Stephane, et al.
(författare)
-
Temporal logics in computer science : Finite-state systems
- 2016
-
Bok (övrigt vetenskapligt/konstnärligt)abstract
- This comprehensive text provides a modern and technically precise exposition of the fundamental theory and applications of temporal logics in computer science. Part I presents the basics of discrete transition systems, including constructions and behavioural equivalences. Part II examines the most important temporal logics for transition systems and Part III looks at their expressiveness and complexity. Finally, Part IV describes the main computational methods and decision procedures for model checking and model building - based on tableaux, automata and games - and discusses their relationships. The book contains a wealth of examples and exercises, as well as an extensive annotated bibliography. Thus, the book is not only a solid professional reference for researchers in the field but also a comprehensive graduate textbook that can be used for self-study as well as for teaching courses.
|
|
