Explore chapters and articles related to this topic
Assertion-Based Verification
Published in Louis Scheffer, Luciano Lavagno, Grant Martin, EDA for IC System Design, Verification, and Testing, 2018
that represents a forward progression of time and a succession of states, si. When proving a temporal assertion, we may assume that a point in time or given state along the path has a unique future or successor state (for example, s0 → s1), in which case the assertion is checked on a given path or trace of execution (for example, a single simulation trace). Thus, each possible computational path of a system is considered separately. We refer to this form of logic as linear-time temporal logic, and Linear Temporal Logic (LTL) is one example [2]. Alternatively, we may assume that each point in time or given state along a path may split into multiple futures or successor states (for example, s0 → s1 and s0 → s5). In that case, all computational paths are considered concurrently, and are usually represented as a tree of infinite computational paths. We refer to this form of logic as branching-time temporal logic, and Computation Tree Logic (CTL) is one example [3].
Combinatorial diversity metrics for declarative processes: an application to policy process analysis
Published in International Journal of General Systems, 2021
In this paper, we will take as our starting point the paradigm of a declarative process. This declarative approach involves declaring relations between activities in the policy process that may (or may not) happen, and then studying the possible ways (termed traces) in which a policy process may be executed. A natural setting for studying such declarative models is linear temporal logic (LTL), an extension to propositional logic that includes temporal operators. A useful tool in BPM is the Declare language (van der Aalst, Pesic, and Schonenberg 2009) which was developed for modelling LTL expressions. The semantics of Declare is clearer than the corresponding LTL expressions and we adopt the Declare expressions and operators. A common feature of the use of LTL is the appearance of infinite traces. Research in the area has looked at a finite counterparts to LTL that deal with finite traces where this has been needed at an application level for tasks such as specification and verification (Fionda and Greco 2018; Pesic, Bosnacki, and van der Aalst 2010).
Defeasible linear temporal logic
Published in Journal of Applied Non-Classical Logics, 2023
Anasse Chafik, Fahima Cheikh-Alili, Jean-François Condotta, Ivan Varzinczak
Linear Temporal Logic was introduced by Pnueli (1977) as a formal tool for hardware and software specification and verification. This formalism allows for the description of a program's executions. is a modal temporal logic, it uses modalities to refer to time. We can encode sentences that describe the future of an execution, e.g. from now on a statement is always true, or, will eventually hold.