Abstract. This paper explores the use of temporal logics in the context of communication protocols for multiagent systems. We concentrate on frameworks where protocols are used to ...
We present a natural deduction calculus for the computation tree logic CTL defined with the full set of classical and temporal logic operators. The system extends the natural ded...
Alexander Bolotov, Oleg Grigoriev, Vasilyi Shangin
When monitoring a system wrt. a property defined in some temporal logic, e. g., LTL, a major concern is to settle with an adequate interpretation of observable system events; that...
Andreas Bauer 0002, Martin Leucker, Christian Scha...
Abstract. We consider the temporal logic with since and until modalities. This temporal logic is expressively equivalent over the class of ordinals to first-order logic thanks to ...
Abstract. In order to verify programs with pointer variables, we introduce a temporal logic LTLmem whose underlying assertion language is the quantifier-free fragment of separatio...
Modern hardware designs are typically based on multiple clocks. While a singly-clocked hardware design is easily described in standard temporal logics, describing a multiply-clocke...
In abstract algebra, a structure is said to be Noetherian if it does not admit infinite strictly ascending chains of congruences. In this paper, we adapt this notion to first-ord...
ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions...
Abstract. Sequent calculi usually provide a general deductive setting that uniformly embeds other proof-theoretical approaches, such as tableaux methods, resolution techniques, goa...
We study logical properties that concern the preservation of futuredirected obligations that have not been fulfilled yet. Our starting point is a product of temporal and deontic ...