共查询到20条相似文献,搜索用时 15 毫秒
1.
Liveness temporal properties state that something “good” eventually happens, e.g., every request is eventually granted. In
Linear Temporal Logic (LTL), there is no a priori bound on the “wait time” for an eventuality to be fulfilled. That is, F
θ asserts that θ holds eventually, but there is no bound on the time when θ will hold. This is troubling, as designers tend to interpret an eventuality F
θ as an abstraction of a bounded eventuality F
≤k
θ, for an unknown k, and satisfaction of a liveness property is often not acceptable unless we can bound its wait time. We introduce here prompt-LTL, an extension of LTL with the prompt-eventually operator F
p
. A system S satisfies a prompt-LTL formula φ if there is some bound k on the wait time for all prompt-eventually subformulas of φ in all computations of S. We study various problems related to prompt-LTL, including realizability, model checking, and assume-guarantee model checking, and show that they can be solved by techniques
that are quite close to the standard techniques for LTL. 相似文献
2.
《Information Processing Letters》2014,114(12):680-688
We show that deciding whether a TPTL formula describes a safety property is EXPSPACE-complete. Moreover, deciding whether a TPTL formula describes a liveness property is in 2-EXPSPACE. Our algorithms for deciding these problems extend those presented by Sistla [1] to decide the corresponding problems for LTL. 相似文献
3.
We consider concurrent probabilistic systems, based on probabilistic automata of Segala & Lynch [55], which allow non-deterministic
choice between probability distributions. These systems can be decomposed into a collection of “computation trees” which arise
by resolving the non-deterministic, but not probabilistic, choices. The presence of non-determinism means that certain liveness
properties cannot be established unless fairness is assumed. We introduce a probabilistic branching time logic PBTL, based on the logic TPCTL of Hansson [30] and the logic PCTL of [55], resp. pCTL [14]. The formulas of the logic express properties such as “every request is eventually granted with probability at least
p”. We give three interpretations for PBTL on concurrent probabilistic processes: the first is standard, while in the remaining two interpretations the branching time
quantifiers are taken to range over a certain kind of fair computation trees. We then present a model checking algorithm for
verifying whether a concurrent probabilistic process satisfies a PBTL formula assuming fairness constraints. We also propose adaptations of existing model checking algorithms for pCTL
[4, 14] to obtain procedures for PBTL
under fairness constraints. The techniques developed in this paper have applications in automatic verification of randomized
distributed systems.
Received: June 1997 / Accepted: May 1998 相似文献
4.
John Håkansson Bengt Jonsson Ola Lundqvist 《International Journal on Software Tools for Technology Transfer (STTT)》2003,4(4):456-471
This paper is concerned with the problem of checking, by means of testing, that a software component satisfies a specification of temporal safety properties. Checking that an actual observed behavior conforms to the specification is performed by a test oracle, which can be either a human tester or a software module. We present a technique for automatically generating test oracles from specifications of temporal safety properties in a metric temporal logic. The logic can express quantitative timing properties, and can also express properties of data values by means of a quantification construct. The generated oracle works online in the sense that checking is performed simultaneously with observation. The technique has been implemented and used in case studies at Volvo Technical Development Corporation . 相似文献
5.
Cong TianZhenhua Duan 《Theoretical computer science》2011,412(18):1729-1744
This paper investigates the expressiveness of Propositional Projection Temporal Logic with Star (PPTL*). To this end, Büchi automata and ω-regular expressions are first extended as Stutter Büchi Automata (SBA) and Extended Regular Expressions (ERE) to include both finite and infinite strings. Further, by equivalent transformations among PPTL* formulas, SBAs and EREs, PPTL* is proved to represent exactly the full regular language. Moreover, some fragments of PPTL* are characterized, and finally, PPTL* and its fragments are classified into five different language classes. 相似文献
6.
The paper considers the treatment of fairness assumptions which arenot equivalence-robust, a central issue in relatinginterleaving semantics topartial order semantics. A notion ofcompletion is introduced and studied, and two specific completions are considered:maximal completion, which is easier to implement (shown by a broadcast bus implementation) but guarantees only weak liveness properties of programs using it; andminimal completion, which may be harder to implement but induces stronger liveness properties on programs using it. Some properties of completions are formulated. Finally, the impact of non-equivalence-robustness on compositionality with respect to separate fairness assumptions is considered.Work started during a visit of the first author to the Computer Science Department, Abo Akademi, Finland, July–August 1988, and continued during the first author's stay at MCC in 1989/90. 相似文献
7.
8.
9.
《国际计算机数学杂志》2012,89(10):1203-1211
The model of concurrent uninterpreted transactions [Papadimitriou, C. H. (1979). The serializability of concurrent database updates. J. ACM, 26, 631–653.] is extended to histories with infinitely many occurrences of the transactions. Such histories are viewed as models of linear temporal logic formulae with propositions representing read and write steps of transactions. A necessary and sufficient condition for histories to be serializable is encoded into temporal logic by the use of propositional quantification. The encoding differs from work on commutativity-based serializability and partial-order temporal logics in using linear temporal logic and defining serializability in terms of uninterpreted histories without reference to the state of variables. An application is the specification of a weaker form of serializability where commutativity of steps is not determined by past history. 相似文献
10.
David Scholefield 《Formal Aspects of Computing》1996,8(4):408-427
A refinement calculus for the development of real-time systems is presented. The calculus is based upon a wide-spectrum language called TAM (the Temporal Agent Model), within which both functional and timing properties can be expressed in either abstract or concrete terms. A specification oriented semantics is given for the language. Program development is considered as a refinement process i.e. thecalculation of a structured program from an unstructured specification. An example program is developed. 相似文献
11.
Currently known sequent systems for temporal logics such as linear time temporal logic and computation tree logic either rely on a cut rule, an invariant rule, or an infinitary rule. The first and second violate the subformula property and the third has infinitely many premises. We present finitary cut-free invariant-free weakening-free and contraction-free sequent systems for both logics mentioned. In the case of linear time all rules are invertible. The systems are based on annotating fixpoint formulas with a history, an approach which has also been used in game-theoretic characterisations of these logics. 相似文献
12.
Lock-freedom is a property of concurrent programs which states that, from any state of the program, eventually some process will complete its operation. Lock-freedom is a weaker property than the usual expectation that eventually all processes will complete their operations. By weakening their completion guarantees, lock-free programs increase the potential for parallelism, and hence make more efficient use of multiprocessor architectures than lock-based algorithms. However, lock-free algorithms, and reasoning about them, are considerably more complex.In this paper we present a technique for proving that a program is lock-free. The technique is designed to be as general as possible and is guided by heuristics that simplify the proofs. We demonstrate our theory by proving lock-freedom of two non-trivial examples from the literature. The proofs have been machine-checked by the PVS theorem prover, and we have developed proof strategies to minimise user interaction. 相似文献
13.
This paper presents a temporal logic formulation of discrete event control which forms a new theoretical basis for control analysis and synthesis of a class of discrete event systems (DES). Based on the formulation, a basic supervisory control theory is developed for a control objective specified by an invariance formula belonging to the safety canonical class of Manna and Pneuli. Using the safety canonical class as a basis, the refinement and generalization of the existing basic predicate framework are demonstrated. A simple example illustrates the formal axiomatic means to perform control-theoretic analysis and synthesis under the new formulation. 相似文献
14.
15.
Proving pointer programs in higher-order logic 总被引:2,自引:0,他引:2
Building on the work of Burstall, this paper develops sound modelling and reasoning methods for imperative programs with pointers: heaps are modelled as mappings from addresses to values, and pointer structures are mapped to higher-level data types for verification. The programming language is embedded in higher-order logic. Its Hoare logic is derived. The whole development is purely definitional and thus sound. Apart from some smaller examples, the viability of this approach is demonstrated with a non-trivial case study. We show the correctness of the Schorr–Waite graph marking algorithm and present part of its readable proof in Isabelle/HOL. 相似文献
16.
Michael Fisher 《Formal Aspects of Computing》1992,4(3):299-319
This report describes the design and implementation of a model checker for linear time temporal logic. The model checker uses a depth-first search algorithm that attempts to find a minimal satisfying model and uses as little space as possible during the checking procedure. The depth-first nature of the algorithm enables the model checker to be used where space is at a premium.This work was supported both by Alvey under grant PRJ/SE/054 (SERC grant GR/D/57942) and by ESPRIT under Basic Research Action 3096 (SPEC). 相似文献
17.
Medha Bhargava Chia-Chih Chen M. S. Ryoo J. K. Aggarwal 《Machine Vision and Applications》2009,20(5):271-281
This paper describes a novel framework for a smart threat detection system that uses computer vision to capture, exploit and
interpret the temporal flow of events related to the abandonment of an object. Our approach uses contextual information along
with an analysis of the causal progression of events to decide whether or not an alarm should be raised. When an unattended
object is detected, the system traces it back in time to determine and record who its most likely owner(s) may be. Through
subsequent frames, the system searches the scene for the owner and issues an alert if no match is found for the owner over
a given period of time. Our algorithm has been successfully tested on two benchmark datasets (PETS 2006 Benchmark Data, 2006;
i-LIDS Dataset for AVSS, 2007), and yielded results that are substantially more accurate than similar systems developed by
other academic and industrial research groups. 相似文献
18.
Timing and liveness in continuous Petri nets 总被引:1,自引:0,他引:1
Fluidification constitutes a relaxation technique for studying discrete event systems through fluidified approximated models, thus avoiding the state explosion problem. Moreover, the class of continuous models thus obtained may be interesting in itself. In Petri nets, fluidification leads to the so-called continuous Petri nets, which are technically hybrid models. Under infinite server semantics, timing a continuous Petri net model preserves the liveness property, but the converse is not necessarily true, and if the autonomous net model is not live, the timing may transform it into a live model. In this paper, we investigate the conditions on the firing rates of timed continuous models that make a given continuous system live. 相似文献
19.
行为时态逻辑TLA(temporal logic of actions)能够在一种语言中同时表达模型程序与逻辑规则,是目前模型检测技术中一个较新的研究方向.为了理解行为时态逻辑与传统时态逻辑之间的理论联系,研究了时态逻辑的语义和定理系统,并根据行为时态逻辑TLA的自身特征指出了TLA中的行为属于时态逻辑T4系统.在此基础上严格的证明了TIA的定理系统及TLA中强公平性蕴涵弱公平性的重要性质,讨论了强公平性与弱公平性等价的条件.最后以实例说明了如何确定动作的强弱公平性,进而建立系统的TLA模型. 相似文献
20.
This paper presentes a novel resolution method,T-resolution,based on the first order temporal logic.The primary claim of this method is its soundness and completeness.For this purpose,we construct the corresponding semantic trees and extend Herbrand‘s Theorem. 相似文献