Commenced in January 2007
Frequency: Monthly
Edition: International
Paper Count: 2

Search results for: computational tree logic

2 A CTL Specification of Serializability for Transactions Accessing Uniform Data

Authors: Rafat Alshorman, Walter Hussak

Abstract:

Existing work in temporal logic on representing the execution of infinitely many transactions, uses linear-time temporal logic (LTL) and only models two-step transactions. In this paper, we use the comparatively efficient branching-time computational tree logic CTL and extend the transaction model to a class of multistep transactions, by introducing distinguished propositional variables to represent the read and write steps of n multi-step transactions accessing m data items infinitely many times. We prove that the well known correspondence between acyclicity of conflict graphs and serializability for finite schedules, extends to infinite schedules. Furthermore, in the case of transactions accessing the same set of data items in (possibly) different orders, serializability corresponds to the absence of cycles of length two. This result is used to give an efficient encoding of the serializability condition into CTL.

Keywords: computational tree logic, serializability, multi-step transactions.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 834
1 CBCTL: A Reasoning System of TemporalEpistemic Logic with Communication Channel

Authors: Suguru Yoshioka, Satoshi Tojo

Abstract:

This paper introduces a temporal epistemic logic CBCTL that updates agent-s belief states through communications in them, based on computational tree logic (CTL). In practical environments, communication channels between agents may not be secure, and in bad cases agents might suffer blackouts. In this study, we provide inform* protocol based on ACL of FIPA, and declare the presence of secure channels between two agents, dependent on time. Thus, the belief state of each agent is updated along with the progress of time. We show a prover, that is a reasoning system for a given formula in a given a situation of an agent ; if it is directly provable or if it could be validated through the chains of communications, the system returns the proof.

Keywords: communication channel, computational tree logic, reasoning system, temporal epistemic logic.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 845