5 found
Order:
  1.  39
    An Alternating-Time Temporal Logic with Knowledge, Perfect Recall and Past: Axiomatisation and Model-Checking.Dimitar P. Guelev, Catalin Dima & Constantin Enea - 2011 - Journal of Applied Non-Classical Logics 21 (1):93-131.
    We present a variant of ATL with incomplete information which includes the distributed knowledge operators corresponding to synchronous action and perfect recall. The cooperation modalities assume the use the distributed knowledge of coalitions and accordingly refer to perfect recall incomplete information strategies. We propose a model-checking algorithm for the logic. It is based on techniques for games with imperfect information and partially observable objectives, and involves deciding emptiness for automata on infinite trees. We also propose an axiomatic system and prove (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  2. A Separation Theorem for Discrete-Time Interval Temporal Logic.Dimitar P. Guelev & Ben Moszkowski - 2022 - Journal of Applied Non-Classical Logics 32 (1):28-54.
    Gabbay's separation theorem about linear temporal logic with past has proved to be one of the most useful theoretical results in temporal logic. In this paper, we establish an analogous statement a...
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  3.  34
    A Relatively Complete Axiomatisation of Projection Onto State in the Duration Calculus.Dimitar P. Guelev & Dang Van Hung - 2004 - Journal of Applied Non-Classical Logics 14 (1-2):149-180.
    We present a complete axiomatisation of the operator of projection onto state in the Duration Calculus relative to validity in DC without extending constructs. Projection onto state was introduced and studied extensively in our earlier works. We first establish the completeness of a system of axioms and proof rules for the operator relative to validity in the extension of DC by neighbourhood formulas, which express the neighbourhood values of boolean DC state expressions. By establishing a relatively complete axiomatisation for the (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  4.  36
    Logical Interpolation and Projection Onto State in the Duration Calculus.Dimitar P. Guelev - 2004 - Journal of Applied Non-Classical Logics 14 (1-2):181-208.
    We generalise an interval-related interpolation theorem about abstract-time Interval Temporal Logic, which was first obtained in [GUE 01]. The generalisation is based on the abstract-time variant of a projection operator in the Duration Calculus, which was introduced in [DAN 99] and later studied extensively in [GUE 02]. We propose a way to understand interpolation in the context of formal verification. We give an example showing that, unlike abstract-time ITL, DC does not have the Craig interpolation property in general, and establish (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  5.  36
    A Propositional Dynamic Logic with Qualitative Probabilities.Dimitar P. Guelev - 1999 - Journal of Philosophical Logic 28 (6):575-604.
    This paper presents an w-completeness theorem for a new propositional probabilistic logic, namely, the dynamic propositional logic of qualitative probabilities (DQP), which has been introduced by the author as a dynamic extension of the logic of qualitative probabilities (Q P) introduced by Segerberg.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark