Change search
Refine search result
1 - 31 of 31
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Rows per page
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sort
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
Select
The maximal number of hits you can export is 250. When you want to export more records please use the Create feeds function.
  • 1. Aceto, Luca
    et al.
    Della Monica, Dario
    Goranko, Valentin
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    Ingólfsdóttir, Anna
    Montanari, Angelo
    Sciavicco, Guido
    A complete classification of the expressiveness of interval logics of Allen’s relations: the general and the dense cases2016In: Acta Informatica, ISSN 0001-5903, E-ISSN 1432-0525, Vol. 53, no 3, p. 207-246Article in journal (Refereed)
    Abstract [en]

    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.
    Goranko, Valentin
    Stockholm University, Faculty of Humanities, Department of Philosophy.
    Jamroga, Wojciech
    Logics for reasoning about strategic abilities in multi-player games2015In: Models of strategic reasoning: logics, games and communities / [ed] Johan van Benthem, Sujata Ghosh, Rineke Verbrugge, Berlin: Springer, 2015, p. 93-136Chapter in book (Refereed)
    Abstract [en]

    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.
    David, Amélie
    Goranko, Valentin
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    Minimisation of Models Satisfying CTL Formulas2019In: 26th International Symposium on Temporal Representation and Reasoning (TIME 2019) / [ed] Johann Gamper, Sophie Pinchinat, Guido Sciavicco, 2019, p. 13:1-13:15, article id 13Conference paper (Refereed)
    Abstract [en]

    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.
    David, Amélie
    Goranko, Valentin
    Stockholm University, Faculty of Humanities, Department of Philosophy.
    Optimal Tableaux Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-time Temoral Logic ATL+2015In: ACM Transactions on Computational Logic, ISSN 1529-3785, E-ISSN 1557-945X, Vol. 17, no 1, article id 4Article in journal (Refereed)
    Abstract [en]

    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. Condurache, Rodica
    et al.
    De Masellis, Riccardo
    Stockholm University, Faculty of Humanities, Department of Philosophy.
    Goranko, Valentin
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    Dynamic Multi-Agent Systems: Conceptual Framework, Automata-Based Modelling and Verification2019In: PRIMA 2019: Principles and Practice of Multi-Agent Systems: Proceedings / [ed] Matteo Baldoni, Mehdi Dastani, Beishui Liao, Yuko Sakurai, Rym Zalila Wenkstern, Springer, 2019, p. 106-122Conference paper (Refereed)
    Abstract [en]

    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.

  • 6. Conradie, Willem
    et al.
    Goranko, Valentin
    Stockholm University, Faculty of Humanities, Department of Philosophy.
    Logic and Discrete Mathematics: a Concise Introduction2015Book (Refereed)
    Abstract [en]

    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.

  • 7. Conradie, Willem
    et al.
    Goranko, Valentin
    Stockholm University, Faculty of Humanities, Department of Philosophy.
    Robinson, Claudette
    Logic and Discrete Mathematics: a Concise Introduction, Solutions Manual2015Book (Other academic)
    Abstract [en]

    Solutions manual to accompany Logic and Discrete Mathematics: A Concise Introduction

  • 8.
    De Masellis, Riccardo
    et al.
    Stockholm University, Faculty of Humanities, Department of Philosophy.
    Goranko, Valentin
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    Gruner, Stefan
    Timm, Nils
    Generalising the Dining Philosophers Problem: Competitive Dynamic Resource Allocation in Multi-agent Systems2019In: Multi-Agent Systems: Revised Selected Papers / [ed] Marija Slavkovik, Springer, 2019, p. 30-47Conference paper (Refereed)
    Abstract [en]

    We consider a new generalisation of the Dining Philosophers problem with a set of agents and a set of resource units which can be accessed by them according to a fixed graph of accessibility between agents and resources. Each agent needs to accumulate a certain (fixed for the agent) number of accessible resource units to accomplish its task, and once it is accomplished the agent releases all resources and starts accumulating them again. All this happens in succession of discrete ‘rounds’ and yields a concurrent game model of ‘dynamic resource allocation’. We use the Alternating time Temporal Logic (ATL) to specify important properties, such as goal achievability, fairness, deadlock, starvation, etc. These can be formally verified using the efficient model checking algorithm for ATL. However, the sizes of the resulting explicit concurrent game models are generally exponential both in the number of resources and the number of agents, which makes the ATL model checking procedure generally intractable on such models, especially when the number of resources is large. That is why we also develop an abstract representation of the dynamic resource allocation models and develop a symbolic version of the model checking procedure for ATL. That symbolic procedure reduces the time complexity of model checking to polynomial in the number of resources, though it can take a worst-case double exponential time in the number of agents.

  • 9. Demri, Stephane
    et al.
    Goranko, Valentin
    Stockholm University, Faculty of Humanities, Department of Philosophy.
    Lange, Martin
    Temporal logics in computer science: Finite-state systems2016Book (Other academic)
    Abstract [en]

    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.

  • 10. Fernández-Duque, David
    et al.
    Goranko, Valentin
    Stockholm University, Faculty of Humanities, Department of Philosophy.
    Secure aggregation of distributed information: How a team of agents can safely share secrets in front of a spy2016In: Discrete Applied Mathematics, ISSN 0166-218X, E-ISSN 1872-6771, Vol. 198, p. 118-135Article in journal (Refereed)
    Abstract [en]

    We consider the generic problem of Secure Aggregation of Distributed Information (SADI), where several agents acting as a team have information distributed amongst them, modelled by means of a publicly known deck of cards distributed amongst the agents, so that each of them knows only her cards. The agents have to exchange and aggregate the information about how the cards are distributed amongst them by means of public announcements over insecure communication channels, intercepted by an adversary “eavesdropper”, in such a way that the adversary does not learn who holds any of the cards. We present a combinatorial construction of protocols that provides a direct solution of a class of SADI problems and develop a technique of iterated reduction of SADI problems to smaller ones which are eventually solvable directly. We show that our methods provide a solution to a large class of SADI problems, including all SADI problems with sufficiently large size and sufficiently balanced card distributions.

  • 11. Gasquet, Olivier
    et al.
    Goranko, Valentin
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    Schwarzentruber, François
    Big Brother Logic: visual-epistemic reasoning in stationary multi-agent systems2016In: Autonomous Agents and Multi-Agent Systems, ISSN 1387-2532, E-ISSN 1573-7454, Vol. 30, no 5, p. 793-825Article in journal (Refereed)
    Abstract [en]

    We consider multi-agent scenarios where each agent controls a surveillance camera in the plane, with fixed position and angle of vision, but rotating freely. The agents can thus observe the surroundings and each other. They can also reason about each other’s observation abilities and knowledge derived from these observations. We introduce suitable logical languages for reasoning about such scenarios which involve atomic formulae stating what agents can see, multi-agent epistemic operators for individual, distributed and common knowledge, as well as dynamic operators reflecting the ability of cameras to turn around in order to reach positions satisfying formulae in the language. We also consider effects of public announcements. We introduce several different but equivalent versions of the semantics for these languages, discuss their expressiveness and provide translations in PDL style. Using these translations we develop algorithms and obtain complexity results for model checking and satisfiability testing for the basic logic BBL that we introduce here and for some of its extensions. Notably, we show that even for the extension with common knowledge, model checking and satisfiability testing remain in PSPACE. We also discuss the sensitivity of the set of validities to the admissible angles of vision of the agents’ cameras. Finally, we discuss some further extensions: adding obstacles, positioning the cameras in 3D or enabling them to change positions. Our work has potential applications to automated reasoning, formal specification and verification of observational abilities and knowledge of multi-robot systems.

  • 12.
    Goranko, Valentin
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    Hybrid Deduction–Refutation Systems2019In: Axioms, E-ISSN 2075-1680, Vol. 8, no 4, article id 118Article in journal (Refereed)
    Abstract [en]

    Hybrid deduction–refutation systems are deductive systems intended to derive both valid and non-valid, i.e., semantically refutable, formulae of a given logical system, by employing together separate derivability operators for each of these and combining ‘hybrid derivation rules’ that involve both deduction and refutation. The goal of this paper is to develop a basic theory and ‘meta-proof’ theory of hybrid deduction–refutation systems. I then illustrate the concept on a hybrid derivation system of natural deduction for classical propositional logic, for which I show soundness and completeness for both deductions and refutations.

  • 13.
    Goranko, Valentin
    Stockholm University, Faculty of Humanities, Department of Philosophy.
    Logic as a Tool: A Guide to Formal Logical Reasoning2016Book (Other academic)
    Abstract [en]

    The book explains the grammar, semantics and use of classical logical languages and teaches the reader how grasp the meaning and translate them to and from natural language.  It illustrates with extensive examples the use of the most popular deductive systems -- axiomatic systems, semantic tableaux, natural deduction, and resolution -- for formalising and automating logical reasoning both on propositional and on first-order level,  and provides the reader with technical skills needed for practical derivations in them.  Systematic guidelines are offered on how to perform logically correct and well-structured reasoning using these deductive systems and the reasoning techniques that they employ. 

  • 14.
    Goranko, Valentin
    et al.
    Stockholm University, Faculty of Humanities, Department of Philosophy.
    Dam, Mads
    Computer Science Logic 20172017Conference proceedings (editor) (Refereed)
    Abstract [en]

    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.

  • 15.
    Goranko, Valentin
    et al.
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    Enqvist, Sebastian
    Stockholm University, Faculty of Humanities, Department of Philosophy.
    Socially Friendly and Group Protecting Coalition Logics2018In: Proceedings of the 17th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2018) / [ed] Mehdi Dastani, Gita Sukthankar, Elisabeth André, Sven Koenig, The International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS), 2018, p. 372-380Conference paper (Refereed)
    Abstract [en]

    We consider extensions of Coalition Logic (CL) which can express statements about inter-related powers of coalitions to achieve their respective goals. In particular, we introduce and study two new extensions of CL. One of them is the “Socially Friendly Coalition Logic” SFCL, which is also a multi-agent extension of the recently introduced “Instantial Neighborhood Logic” INL. SFCL can express the claim that a coalition has a collective strategy to guarantee achieving its explicitly stated goal while acting in a ‘socially friendly way’, by enabling the remaining agents to achieve other (again, explicitly stated) goals of their choice. The other new extension is the “Group Protecting Coalition Logic” GPCL which enables reasoning about entire coalitional goal assignments, in which every group of agents has its own specified goal. GPCL can express claims to the effect that there is an action profile of the grand coalition such that, by playing it, every sub-coalition of agents can guarantee satisfaction of its own private goal (and thus, protect its own interests) while acting towards achievement of the common goal of the grand coalition. For each of these logics, we discuss its expressiveness, introduce the respective notion of bisimulation and prove bisimulation invariance and Hennessy-Milner property. We then also present sound and complete axiomatic systems and prove decidability for both logics.

  • 16.
    Goranko, Valentin
    et al.
    Stockholm University, Faculty of Humanities, Department of Philosophy.
    Galton, Antony
    Temporal Logic2015In: Stanford Encyclopedia of Philosophy, ISSN 1095-5054, E-ISSN 1095-5054Article in journal (Refereed)
  • 17.
    Goranko, Valentin
    et al.
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    Jamroga, Wojciech
    State and Path Coalition Effectivity Models for Logics of Multi-Player Games2016In: Autonomous Agents and Multi-Agent Systems, ISSN 1387-2532, E-ISSN 1573-7454, Vol. 30, no 3, p. 446-485Article in journal (Refereed)
    Abstract [en]

    We consider models of multi-player games where abilities of players and coalitions are defined in terms of sets of outcomes which they can effectively enforce. We extend the well-studied state effectivity models of one-step games in two different ways. On the one hand, we develop multiple state effectivity functions associated with different long-term temporal operators. On the other hand, we define and study coalitional path effectivity models where the outcomes of strategic plays are infinite paths. For both extensions we obtain representation results with respect to concrete models arising from concurrent game structures. We also apply state and path coalitional effectivity models to provide alternative, arguably more natural and elegant semantics to the alternating-time temporal logic ATL*, and discuss their technical and conceptual advantages.

  • 18.
    Goranko, Valentin
    et al.
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    Ju, Fengkui
    Towards a Logic for Conditional Local Strategic Reasoning2019In: Logic, Rationality, and Interaction: Proceedings / [ed] Patrick Blackburn, Emiliano Lorini, Meiyun Guo, Springer, 2019, p. 112-125Conference paper (Refereed)
    Abstract [en]

    We consider systems of rational agents who act in pursuit of their individual and collective objectives and we study the reasoning of an agent or an external observer about the consequences from the expected choices of action of the other agents based on their objectives, in order to assess the reasoner’s ability to achieve his own objective.

    To formalize such reasoning we introduce new modal operators of conditional strategic reasoning and use them to extend Coalition Logic in order to capture variations of conditional strategic reasoning. We provide formal semantics for the new conditional strategic operators, introduce the matching notion of bisimulation for each of them and discuss and compare briefly their expressiveness.

  • 19.
    Goranko, Valentin
    et al.
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    Kuijer, Louwe B.
    On the Length and Depth of Temporal Formulae Distinguishing Non-bisimilar Transition Systems2016In: 23rd International Symposium on Temporal Representation and Reasoning: Proceedings / [ed] Curtis Dyreson, Michael R. Hansen, Luke Hunsberger, IEEE Computer Society, 2016, p. 177-185Conference paper (Refereed)
    Abstract [en]

    We investigate the minimal length and nesting depth of temporal formulae that distinguish two given non-bisimilar finite pointed transition systems. We show that such formula can always be constructed in length at most exponential in the combined number of states of both transition systems, and give an example with exponential lower bound, for several common temporal languages. We then show that by using renamings of subformulae or explicit assignments the length of the distinguishing formula can always be reduced to one that is bounded above by a cubic polynomial on the combined size of both transition systems. This is also a bound for the size obtained by using DAG representation of formulae. We also prove that the minimal nesting depth for such formula is less than the combined size of the two state spaces and obtain some tight upper bounds.

  • 20.
    Goranko, Valentin
    et al.
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    Kuusisto, Antti
    LOGICS FOR PROPOSITIONAL DETERMINACY AND INDEPENDENCE2018In: The Review of Symbolic Logic, ISSN 1755-0203, E-ISSN 1755-0211, Vol. 11, no 3, p. 470-506Article in journal (Refereed)
    Abstract [en]

    We introduce and study formal logics for reasoning about propositional determinacy and independence. These relate naturally with the philosophical concept of supervenience, which can also be regarded as a generalisation of logical consequence. Propositional Dependence Logic D, and Propositional Independence Logic I are recently developed logical systems, based on team semantics, that provide a framework for such reasoning tasks. We introduce two new logics L_D and L_I, based on Kripke semantics, and propose them as alternatives for D and I, respectively. We analyse and compare the relative expressive powers of these four logics and also discuss how they relate to the natural language use and meaning of the concepts of determinacy and independence. We argue that L_D and L_I naturally resolve a range of interpretational problems that arise in D and I. We also obtain sound and complete axiomatizations for L_D and L_I and relate them with the recently studied inquisitive logics and their semantics.

  • 21.
    Goranko, Valentin
    et al.
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    Kuusisto, Antti
    Rönnholm, Raine
    Alternating-time temporal logic ATL with finitely bounded semantics2019In: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 797, p. 129-155Article in journal (Refereed)
    Abstract [en]

    We study a variant ATL(FB) of the alternating-time temporal logic ATL with a nonstandard, 'finitely bounded' semantics (FBS). FBS was originally defined as a game-theoretic semantics where players must commit to time limits when attempting to verify eventuality (respectively, to falsify safety) formulae. It turns out that FBS has a natural corresponding compositional semantics that essentially evaluates formulae only on finite initial segments of paths and imposes uniform bounds on all plays for the fulfilment of eventualities. The resulting version ATL(FB) differs in some essential features from the standard ATL, as it no longer has the finite model property, though the two logics are equivalent on finite models. We develop two tableau systems for ATL(FB). The first one deals with infinite sets of formulae and may run in a transfinite sequence of steps, whereas the second one deals only with finite sets of formulae in an extended language allowing explicit symbolic indication of time limits in formulae. We prove soundness and completeness of the infinitary tableau system and prove that it is equivalent to the finitary one. We also show that the finitary tableau system provides an exponential-time decision procedure for the satisfiability problem of ATL(FB) and thus establishes its EXPTIME-completeness. Furthermore, we present an infinitary axiomatization for ATL(FB) and prove its soundness and completeness. 

  • 22.
    Goranko, Valentin
    et al.
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    Kuusisto, Antti
    Rönnholm, Raine
    CTL with finitely bounded semantics2017In: 24th International Symposium on Temporal Representation and Reasoning (TIME 2017) / [ed] Sven Schewe, Thomas Schneider, Jef Wijsen, Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik , 2017, p. 14:1-14:19Conference paper (Refereed)
    Abstract [en]

    We consider a variation of the branching time logic CTL with non-standard, "finitely bounded" semantics (FBS). FBS is naturally defined as game-theoretic semantics where the proponent of truth of an eventuality must commit to a time limit (number of transition steps) within which the formula should become true on all (resp. some) paths starting from the state where the formula is evaluated. The resulting version CTL(FB) of CTL differs essentially from the standard one as it no longer has the finite model property. We develop two tableaux systems for CTL(FB). The first one deals with infinite sets of formulae, whereas the second one deals with finite sets of formulae in a slightly extended language allowing explicit indication of time limits in formulae. We prove soundness and completeness of both systems and also show that the latter tableaux system provides an EXPTIME decision procedure for it and thus prove EXPTIME-completeness of the satisfiability problem.

  • 23.
    Goranko, Valentin
    et al.
    Stockholm University, Faculty of Humanities, Department of Philosophy.
    Kuusisto, Antti
    University of Bremen, Germany.
    Rönnholm, Raine
    University of Tampere, Finland.
    Game-Theoretic Semantics for Alternating-Time Temporal Logic2016In: Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems / [ed] J. Thangarajah, K. Tuyls, C. M. Jonker, S. Marsella, The International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS), 2016, p. 671-679Conference paper (Refereed)
    Abstract [en]

    We introduce versions of game-theoretic semantics (GTS) for Alternating-Time Temporal Logic (ATL). In GTS, truth is defined in terms of existence of a winning strategy in a semantic evaluation game, and thus the game-theoretic perspective appears in the framework of ATL on two semantic levels: on the object level, in the standard semantics of the strategic operators, and on the meta-level, where game-theoretic logical semantics can be applied to ATL. We unify these two perspectives into semantic evaluation games specially designed for ATL. The novel game-theoretic perspective enables us to identify new variants of the semantics of ATL, based on limiting the time resources available to the verifier and falsifier in the semantic evaluation game; we introduce and analyse an unbounded and bounded GTS and prove these to be equivalent to the standard (Tarski-style) compositional semantics. We also introduce a non-equivalent finitely bounded semantics and argue that it is natural from both logical and game-theoretic perspectives.

  • 24.
    Goranko, Valentin
    et al.
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    Kuusisto, Antti
    Rönnholm, Raine
    Game-Theoretic Semantics for Alternating-Time Temporal Logic2018In: ACM Transactions on Computational Logic, ISSN 1529-3785, E-ISSN 1557-945X, Vol. 19, no 3, article id 17Article in journal (Refereed)
    Abstract [en]

    We introduce several versions of game-theoretic semantics (GTS) for Alternating-Time Temporal Logic (ATL). In GTS, truth is defined in terms of existence of a winning strategy in a semantic evaluation game. Thus, the game-theoretic perspective appears in the framework of ATL on two semantic levels: on the object level in the standard semantics of the strategic operators and on the meta-level, where game-theoretic logical semantics is applied to ATL. We unify these two perspectives into semantic evaluation games specially designed for ATL. The game-theoretic perspective enables us to identify new variants of the semantics of ATL based on limiting the time resources available to the verifier and falsifier in the semantic evaluation game. We introduce and analyze an unbounded and (ordinal) bounded GTS and prove these to be equivalent to the standard (Tarski-style) compositional semantics. We show that, in bounded GTS, truth of ATL formulae can always be determined in finite time, that is, without constructing infinite paths. We also introduce a nonequivalent finitely bounded semantics and argue that it is natural from both logical and game-theoretic perspectives.

  • 25.
    Goranko, Valentin
    et al.
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    Kuusisto, Antti
    Rönnholm, Raine
    Game-Theoretic Semantics for ATL+ with Applications to Model Checking2017In: Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems (AAMAS'2017) / [ed] S. Das, E. Durfee, K. Larson, M. Winikoff, The International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS), 2017, p. 1277-1285Conference paper (Refereed)
    Abstract [en]

    We develop a game-theoretic semantics (GTS) for the fragment ATL+ of the Alternating-time Temporal Logic ATL∗, essentially extending a recently introduced GTS for ATL. We show that the new game-theoretic semantics is equivalent to the standard compositional semantics of ATL+ (with perfect-recall strategies). Based on the new semantics, we providean analysis of the memory and time resources needed formodel checking ATL+ and show that strategies of the verifier that use only a very limited amount of memory suffice. Furthermore, using the GTS we provide a new algorithm for model checking ATL+ and identify a natural hierarchy of tractable fragments of ATL+ that extend ATL.

  • 26.
    Goranko, Valentin
    et al.
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    Kuusisto, Antti
    Rönnholm, Raine
    Rational Coordination in Games with Enriched Representations2018In: Multi-Agent Systems and Agreement Technologies: Revised Selected Papers / [ed] Francesco Belardinelli, Estefanía Argente, Springer, 2018, p. 323-338Conference paper (Refereed)
    Abstract [en]

    We consider pure win-lose coordination games where the representation of the game structure has additional features that are commonly known to the players, such as colouring, naming, or ordering of the available choices or of the players. We study how the information provided by such enriched representations affects the solvability of these games by means of principles of rational reasoning in coordination scenarios with no prior communication or conventions.

  • 27.
    Goranko, Valentin
    et al.
    Stockholm University, Faculty of Humanities, Department of Philosophy.
    Kuusisto, Antti
    University of Bremen, Germany.
    Rönnholm, Raine
    University of Tampere, Finland.
    Rational coordination with no communication or conventions2017In: Proceedings of the 6th International Conference on Logic, Rationality and Interaction (LORI VI) / [ed] Alexandru Baltag, Jeremy Seligman, Tomoyuki Yamada, Springer, 2017, p. 33-48Conference paper (Refereed)
    Abstract [en]

    We study pure coordination games where in every outcome, all players have identical payoffs, ‘win’ or ‘lose’. We identify and discuss a range of ‘purely rational principles’ guiding the reasoning of rational players in such games and analyse which classes of coordination games can be solved by such players with no preplay communication or conventions. We observe that it is highly nontrivial to delineate a boundary between purely rational principles and other decision methods, such as conventions, for solving such coordination games.

  • 28.
    Goranko, Valentin
    et al.
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    Turrini, Paolo
    Two-player preplay negotiation games with conditional offers2016In: International Game Theory Review, ISSN 0219-1989, Vol. 18, no 1, article id 1550017Article in journal (Refereed)
    Abstract [en]

    We consider an extension of strategic normal form games with a phase before the actual play of the game, where players can make binding offers for transfer of utilities to other players after the play of the game, contingent on the recipient playing the strategy indicated in the offer. Such offers transform the payoff matrix of the original game but preserve its non-cooperative nature. The type of offers we focus on here are conditional on a suggested matching offer of the same kind made in return by the receiver. Players can exchange a series of such offers, thus engaging in a bargaining process before a strategic normal form game is played. In this paper we study and analyse solution concepts for two-player normal form games with such preplay negotiation phase, under several assumptions for the bargaining power of the players, as well as the value of time for the players in such negotiations. We obtain results describing the possible solutions of such bargaining games and analyse the degrees of efficiency and fairness that can be achieved in such negotiation process. We show the similarities and the differences with a variety of frameworks in the literature of bargaining games and games with a preplay phase. 

  • 29. Ju, Fengkui
    et al.
    Grilletti, Gianluca
    Goranko, Valentin
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    A logic for temporal conditionals and a solution to the Sea Battle Puzzle2018In: Advances in Modal Logic / [ed] Guram Bezhanishvili, Giovanna D'Agostino, George Metcalfe, Thomas Studer, London: College Publications, 2018, p. 379-398Conference paper (Refereed)
    Abstract [en]

    Temporal reasoning with conditionals is more complex than both classical temporal reasoning and reasoning with timeless conditionals, and can lead to some rather counter-intuitive conclusions. For instance, Aristotle’s famous “Sea Battle Tomorrow” puzzle leads to a fatalistic conclusion: whether there will be a sea battle tomorrow or not, but that is necessarily the case now. We propose a branching-time logic LTC to formalise reasoning about temporal conditionals and provide that logic with adequate formal semantics. The logic LTC extends the Nexttime fragment of CTL∗ , with operators for model updates, restricting the domain to only future moments where antecedent is still possible to satisfy. We provide formal semantics for these operators that implements the restrictor interpretation of antecedents of temporalized conditionals, by suitably restricting the domain of discourse. As a motivating example, we demonstrate that a naturally formalised in our logic version of the ‘Sea Battle’ argument renders it unsound, thereby providing a solution to the problem with fatalist conclusion that it entails, because its underlying reasoning per cases argument no longer applies when these cases are treated not as material implications but as temporal conditionals. On the technical side, we analyze the semantics of LTC and provide a series of reductions of LTC-formulae, first recursively eliminating the dynamic update operators and then the path quantifiers in such formulae. Using these reductions we obtain a sound and complete axiomatization for LTC, and reduce its decision problem to that of the modal logic KD.

  • 30. Ju, Fengkui
    et al.
    Grilletti, Gianluca
    Goranko, Valtentin
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    A Logic for Temporal Conditionals and a Solution to the Sea Battle Puzzle2018In: Proceedings of the 12th International Conference on Advances in Modal Logic (AiML'2018) / [ed] Guram Bezhanishvili, Giovanna D'Agostino, George Metcalfe, Thomas Studer, College Publications, 2018, p. 407-426Conference paper (Refereed)
    Abstract [en]

    Temporal reasoning with conditionals is more complex than both classical temporal reasoning and reasoning with timeless conditionals, and can lead to some rather counter-intuitive conclusions. For instance, Aristotle’s famous “Sea Battle Tomorrow” puzzle leads to a fatalistic conclusion: whether there will be a sea battle tomorrow or not, but that is necessarily the case now. We propose a branching-time logic LTC to formalise reasoning about temporal conditionals and provide that logic with adequate formal semantics. The logic LTC extends the Nexttime fragment of CTL∗ , with operators for model updates, restricting the domain to only future moments where antecedent is still possible to satisfy. We provide formal semantics for these operators that implements the restrictor interpretation of antecedents of temporalized conditionals, by suitably restricting the domain of discourse. As a motivating example, we demonstrate that a naturally formalised in our logic version of the ‘Sea Battle’ argument renders it unsound, thereby providing a solution to the problem with fatalist conclusion that it entails, because its underlying reasoning per cases argument no longer applies when these cases are treated not as material implications but as temporal conditionals. On the technical side, we analyze the semantics of LTC and provide a series of reductions of LTC-formulae, first recursively eliminating the dynamic update operators and then the path quantifiers in such formulae. Using these reductions we obtain a sound and complete axiomatization for LTC, and reduce its decision problem to that of the modal logic KD.

  • 31. Ågotnes, Thomas
    et al.
    Goranko, Valentin
    Stockholm University, Faculty of Humanities, Department of Philosophy.
    Jamroga, Wojciech
    Wooldridge, Michael
    Knowledge and Ability2015In: Handbook of Epistemic Logic / [ed] Hans van Ditmarsch. Joseph Halpern, Wiebe van der Hoek and Barteld Kooi, College Publications, 2015, 1, p. 543-589Chapter in book (Refereed)
    Abstract [en]

    In this chapter we relate epistemic logics with logics for strategic ability developed and studied in computer science, artificial intelligence and multi-agent systems. We discuss approaches from philosophy and artificial intelligence to modelling the interaction of agents’ knowledge and abilities and then focus on concurrent game models and the alternating-time temporal logic ATL. We show how ATL enables reasoning about agents’ coalitional abilities to achieve qualitative objectives in concurrent game models, first assuming complete information and then under incomplete information and uncertainty about the structureof the game model. We then discuss epistemic extensions of ATL enabling explicit reasoning about the interaction of knowledge and strategic abilities on different epistemic levels, leading inter alia to the notion of constructive knowledge.

1 - 31 of 31
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf