Log in

Relevant bibliographies by topics / Computation Tree Logics / Journal articles

To see the other types of publications on this topic, follow the link: Computation Tree Logics.

Journal articles on the topic 'Computation Tree Logics'

Author: Grafiati

Published: 6 September 2023

Last updated: 7 September 2023

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles

Select a source type:

Consult the top 50 journal articles for your research on the topic 'Computation Tree Logics.'

Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.

You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.

Browse journal articles on a wide variety of disciplines and organise your bibliography correctly.

1

Kamide, Norihiro. "Logical foundations of hierarchical model checking." Data Technologies and Applications 52, no. 4 (September 4, 2018): 539–63. http://dx.doi.org/10.1108/dta-01-2018-0002.

Full text

Abstract:

Purpose The purpose of this paper is to develop new simple logics and translations for hierarchical model checking. Hierarchical model checking is a model-checking paradigm that can appropriately verify systems with hierarchical information and structures. Design/methodology/approach In this study, logics and translations for hierarchical model checking are developed based on linear-time temporal logic (LTL), computation-tree logic (CTL) and full computation-tree logic (CTL*). A sequential linear-time temporal logic (sLTL), a sequential computation-tree logic (sCTL), and a sequential full computation-tree logic (sCTL*), which can suitably represent hierarchical information and structures, are developed by extending LTL, CTL and CTL*, respectively. Translations from sLTL, sCTL and sCTL* into LTL, CTL and CTL*, respectively, are defined, and theorems for embedding sLTL, sCTL and sCTL* into LTL, CTL and CTL*, respectively, are proved using these translations. Findings These embedding theorems allow us to reuse the standard LTL-, CTL-, and CTL*-based model-checking algorithms to verify hierarchical systems that are modeled and specified by sLTL, sCTL and sCTL*. Originality/value The new logics sLTL, sCTL and sCTL* and their translations are developed, and some illustrative examples of hierarchical model checking are presented based on these logics and translations.

APA, Harvard, Vancouver, ISO, and other styles

2

DALLA CHIARA, MARIA LUISA, ROBERTO GIUNTINI, and ROBERTO LEPORINI. "LOGICS FROM QUANTUM COMPUTATION." International Journal of Quantum Information 03, no. 02 (June 2005): 293–337. http://dx.doi.org/10.1142/s0219749905000943.

Full text

Abstract:

The theory of logical gates in quantum computation has suggested new forms of quantum logic, called quantum computational logics. The basic semantic idea is the following: the meaning of a sentence is identified with a quregister (a system of qubits) or, more generally, with a mixture of quregisters (called qumix). In this framework, any sentence α of the language gives rise to a quantum tree: a kind of quantum circuit that transforms the quregister (qumix) associated to the atomic subformulas of α into the quregister (qumix) associated to α. A variant of the quantum computational semantics is represented by the quantum holistic semantics, which permits us to represent entangled meanings. Physical models of quantum computational logics can be built by means of Mach–Zehnder interferometers.

APA, Harvard, Vancouver, ISO, and other styles

3

Goranko, Valentin. "Temporal Logics with Reference Pointers and Computation Tree Logics." Journal of Applied Non-Classical Logics 10, no. 3-4 (January 2000): 221–42. http://dx.doi.org/10.1080/11663081.2000.10510998.

Full text

APA, Harvard, Vancouver, ISO, and other styles

4

BALTAZAR, P., R. CHADHA, and P. MATEUS. "QUANTUM COMPUTATION TREE LOGIC — MODEL CHECKING AND COMPLETE CALCULUS." International Journal of Quantum Information 06, no. 02 (April 2008): 219–36. http://dx.doi.org/10.1142/s0219749908003530.

Full text

Abstract:

Logics for reasoning about quantum states and their evolution have been given in the literature. In this paper, we consider quantum computation tree logic (QCTL), which adds temporal modalities to exogenous quantum propositional logic. We give a sound and complete axiomatization of QCTL and combine the standard CTL model-checking algorithm with the dEQPL model-checking algorithm to obtain a model-checking algorithm for QCTL. Finally, we illustrate the use of the logic by reasoning about the BB84 key distribution protocol.

APA, Harvard, Vancouver, ISO, and other styles

5

Kamide, Norihiro, and Daiki Koizumi. "Method for Combining Paraconsistency and Probability in Temporal Reasoning." Journal of Advanced Computational Intelligence and Intelligent Informatics 20, no. 5 (September 20, 2016): 813–27. http://dx.doi.org/10.20965/jaciii.2016.p0813.

Full text

Abstract:

Computation tree logic (CTL) is known to be one of the most useful temporal logics for verifying concurrent systems by model checking technologies. However, CTL is not sufficient for handling inconsistency-tolerant and probabilistic accounts of concurrent systems. In this paper, a paraconsistent (or inconsistency-tolerant) probabilistic computation tree logic (PpCTL) is derived from an existing probabilistic computation tree logic (pCTL) by adding a paraconsistent negation connective. A theorem for embedding PpCTL into pCTL is proven, thereby indicating that we can reuse existing pCTL-based model checking algorithms. A relative decidability theorem for PpCTL, wherein the decidability of pCTL implies that of PpCTL, is proven using this embedding theorem. Some illustrative examples involving the use of PpCTL are also presented.

APA, Harvard, Vancouver, ISO, and other styles

6

Walker, Matt, Parssa Khazra, Anto Nanah Ji, Hongru Wang, and Franck van Breugel. "jpf-logic." ACM SIGSOFT Software Engineering Notes 48, no. 1 (January 10, 2023): 32–36. http://dx.doi.org/10.1145/3573074.3573083.

Full text

Abstract:

We present jpf-logic, an extension of the model checker Java PathFinder (JPF). Our extension jpf-logic provides a framework to check properties expressed in temporal logics such as linear temporal logic (LTL) and computation tree logic (CTL). To support a logic in our framework, we (1) implement a parser for the logic, (2) develop a hierarchy of classes that represent the abstract syntax of the logic and implement a transformation from parse trees of formulas to the corresponding abstract syntax trees, and (3) implement a model checking algorithm that takes as input an abstract syntax tree of a formula and a partial transition system. The latter represents a model of the Java application. All three components have been implemented for CTL. The first two have been implemented for LTL.

APA, Harvard, Vancouver, ISO, and other styles

7

JACOBS, BART. "The temporal logic of coalgebras via Galois algebras." Mathematical Structures in Computer Science 12, no. 6 (December 2002): 875–903. http://dx.doi.org/10.1017/s096012950200378x.

Full text

Abstract:

This paper introduces a temporal logic for coalgebras. Nexttime and lasttime operators are defined for a coalgebra, acting on predicates on the state space. They give rise to what is called a Galois algebra. Galois algebras form models of temporal logics like Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). The mapping from coalgebras to Galois algebras turns out to be functorial, yielding indexed categorical structures. This construction gives many examples, for coalgebras of polynomial functors on sets. More generally, it will be shown how ‘fuzzy’ predicates on metric spaces, and predicates on presheaves, yield indexed Galois algebras, in basically the same coalgebraic manner.

APA, Harvard, Vancouver, ISO, and other styles

8

PENCZEK, WOJCIECH. "TEMPORAL LOGICS FOR TRACE SYSTEMS: ON AUTOMATED VERIFICATION." International Journal of Foundations of Computer Science 04, no. 01 (March 1993): 31–67. http://dx.doi.org/10.1142/s0129054193000043.

Full text

Abstract:

We investigate an extension of CTL (Computation Tree Logic) by past modalities, called CTL P, interpreted over Mazurkiewicz’s trace systems. The logic is powerful enough to express most of the partial order properties of distributed systems like serializability of database transactions, snapshots, parallel execution of program segments, or inevitability under concurrency fairness assumption. We show that the model checking problem for the logic is NP-hard, even if past modalities cannot be nested. Then, we give a one exponential time model checking algorithm for the logic without nested past modalities. We show that all the interesting partial order properties can be model checked using our algorithm. Next, we show that is is possible to extend the model checking algorithm to cover the whole language and its extension to [Formula: see text]. Finally, we prove that the logic is undecidable and we discuss consequences of our results on using propositional versions of partial order temporal logics to synthesis of concurrent systems from their specifications.

APA, Harvard, Vancouver, ISO, and other styles

9

Latte, Markus. "Branching-time logics and fairness, revisited." Mathematical Structures in Computer Science 31, no. 9 (October 2021): 1135–44. http://dx.doi.org/10.1017/s0960129521000475.

Full text

Abstract:

AbstractEmerson and Halpern (1986, Journal of the Association for Computing Machinery33, 151–178) prove that the Computation Tree Logic (CTL) cannot express the existence of a path on which a proposition holds infinitely often (fairness for short).The scope is widened from CTL to a general branching-time logic. A path quantifier is followed by a language with temporal descriptions. In this extended setting, the said inexpressiveness is strengthened in two aspects. First, universal path quantifiers are unrestricted. In this way, they are relieved of any temporal quantifiers such as of those in $\mathtt{AU}$ and $\mathtt{AR}$ from CTL. Second, existential path quantifiers are allowed with any countable language. Instances are the temporal quantifiers in $\mathtt{EU}$ and $\mathtt{ER}$ from CTL. By contrast, the fairness statement is an existential path quantifier with an uncountable language. Both aspects indicate that this inexpressiveness is optimal with respect to the polarity of path quantifiers and to the cardinality of their languages.

APA, Harvard, Vancouver, ISO, and other styles

10

Chun, Seung Su. "The Pattern Based Visual Property Specification Language and Supporting System for Software Verifications." Applied Mechanics and Materials 752-753 (April 2015): 1090–96. http://dx.doi.org/10.4028/www.scientific.net/amm.752-753.1090.

Full text

Abstract:

This paper deals with issue of properties specification for software verifications and translation between formal languages. Through this paper, the unique framework of property specifications including most kinds of formal specifications logics, automatic methods are shown by a property specifications guided system and PVSL(The Pattern based Visual property Specification Language).Additionally, a properties to specify and structures, Interconnection of them are also described by property charts. In this study, the pattern based visual property specification language (PVSL) is defined and property specifications method is also designed by convenience specifications of required property.Required properties can be described by its charts and analyzes its meaning and structures as using patterns diagrams and property and-or tree. On the other hands, it also guarantees stability and limitation of utilizations of patterns using much stronger specifying Dwyer`s meaning based property classification. The PVSL and property charts use hierarchical state machine notation to take advantage of knowledge a person who is one of practitioners has as much as possible, and for Nu-SMV, CW-CNC. They can be adapted to describe property charts and analyze into examples of CTL(Computation Tree Logic) and Modal Mu-Calculus logic that have been already used.Keywords: Patterns, Property specifications, model checking, Software verification

APA, Harvard, Vancouver, ISO, and other styles

11

Requeno, José Ignacio, and José Manuel Colom. "Model checking software for phylogenetic trees using distribution and database methods." Journal of Integrative Bioinformatics 10, no. 3 (December 1, 2013): 16–30. http://dx.doi.org/10.1515/jib-2013-229.

Full text

Abstract:

Summary Model checking, a generic and formal paradigm stemming from computer science based on temporal logics, has been proposed for the study of biological properties that emerge from the labeling of the states defined over the phylogenetic tree. This strategy allows us to use generic software tools already present in the industry. However, the performance of traditional model checking is penalized when scaling the system for large phylogenies. To this end, two strategies are presented here. The first one consists of partitioning the phylogenetic tree into a set of subgraphs each one representing a subproblem to be verified so as to speed up the computation time and distribute the memory consumption. The second strategy is based on uncoupling the information associated to each state of the phylogenetic tree (mainly, the DNA sequence) and exporting it to an external tool for the management of large information systems. The integration of all these approaches outperforms the results of monolithic model checking and helps us to execute the verification of properties in a real phylogenetic tree.

APA, Harvard, Vancouver, ISO, and other styles

12

Thomas, Colin, Maximilien Cosme, Cédric Gaucherel, and Franck Pommereau. "Model-checking ecological state-transition graphs." PLOS Computational Biology 18, no. 6 (June 6, 2022): e1009657. http://dx.doi.org/10.1371/journal.pcbi.1009657.

Full text

Abstract:

Model-checking is a methodology developed in computer science to automatically assess the dynamics of discrete systems, by checking if a system modelled as a state-transition graph satisfies a dynamical property written as a temporal logic formula. The dynamics of ecosystems have been drawn as state-transition graphs for more than a century, ranging from state-and-transition models to assembly graphs. Model-checking can provide insights into both empirical data and theoretical models, as long as they sum up into state-transition graphs. While model-checking proved to be a valuable tool in systems biology, it remains largely underused in ecology apart from precursory applications. This article proposes to address this situation, through an inventory of existing ecological STGs and an accessible presentation of the model-checking methodology. This overview is illustrated by the application of model-checking to assess the dynamics of a vegetation pathways model. We select management scenarios by model-checking Computation Tree Logic formulas representing management goals and built from a proposed catalogue of patterns. In discussion, we sketch bridges between existing studies in ecology and available model-checking frameworks. In addition to the automated analysis of ecological state-transition graphs, we believe that defining ecological concepts with temporal logics could help clarify and compare them.

APA, Harvard, Vancouver, ISO, and other styles

13

Bianco, Alessandro, Fabio Mogavero, and Aniello Murano. "Graded computation tree logic." ACM Transactions on Computational Logic 13, no. 3 (August 2012): 1–53. http://dx.doi.org/10.1145/2287718.2287725.

Full text

APA, Harvard, Vancouver, ISO, and other styles

14

Kaneiwa, Ken, and Norihiro Kamide. "Paraconsistent Computation Tree Logic." New Generation Computing 29, no. 4 (October 2011): 391–408. http://dx.doi.org/10.1007/s00354-009-0116-6.

Full text

APA, Harvard, Vancouver, ISO, and other styles

15

Patthak, A. C., I. Bhattacharya, A. Dasgupta, Pallab Dasgupta, and P. P. Chakrabarti. "Quantified Computation Tree Logic." Information Processing Letters 82, no. 3 (May 2002): 123–29. http://dx.doi.org/10.1016/s0020-0190(01)00260-5.

Full text

APA, Harvard, Vancouver, ISO, and other styles

16

Cappello, Peter, and Dimitrios Mourloukos. "CX: A Scalable, Robust Network for Parallel Computing." Scientific Programming 10, no. 2 (2002): 159–71. http://dx.doi.org/10.1155/2002/598245.

Full text

Abstract:

CX, a network-based computational exchange, is presented. The system's design integrates variations of ideas from other researchers, such as work stealing, non-blocking tasks, eager scheduling, and space-based coordination. The object-oriented API is simple, compact, and cleanly separates application logic from the logic that supports interprocess communication and fault tolerance. Computations, of course, run to completion in the presence of computational hosts that join and leave the ongoing computation. Such hosts, or producers, use task caching and prefetching to overlap computation with interprocessor communication. To break a potential task server bottleneck, a network of task servers is presented. Even though task servers are envisioned as reliable, the self-organizing, scalable network ofn- servers, described as asibling-connected height-balanced fat tree, tolerates a sequence ofn-1 server failures. Tasks are distributed throughout the server network via a simple "diffusion" process. CX is intended as a test bed for research on automated silent auctions, reputation services, authentication services, and bonding services. CX also provides a test bed for algorithm research into network-based parallel computation.

APA, Harvard, Vancouver, ISO, and other styles

17

Kaivola, Roope. "Axiomatising extended computation tree logic." Theoretical Computer Science 190, no. 1 (January 1998): 41–60. http://dx.doi.org/10.1016/s0304-3975(97)00083-2.

Full text

APA, Harvard, Vancouver, ISO, and other styles

18

Dasgupta, Pallab, P. P. Chakrabarti, Jatindra Kumar Deka, and Sriram Sankaranarayanan. "Min-max Computation Tree Logic." Artificial Intelligence 127, no. 1 (March 2001): 137–62. http://dx.doi.org/10.1016/s0004-3702(01)00059-5.

Full text

APA, Harvard, Vancouver, ISO, and other styles

19

Baltazar, Pedro, Paulo Mateus, Rajagopal Nagarajan, and Nikolaos Papanikolaou. "Exogenous Probabilistic Computation Tree Logic." Electronic Notes in Theoretical Computer Science 190, no. 3 (September 2007): 95–110. http://dx.doi.org/10.1016/j.entcs.2007.07.007.

Full text

APA, Harvard, Vancouver, ISO, and other styles

20

Котикова, Е. А., and М. Н. Рыбаков. "Kripke Incompleteness of First-order Calculi with Temporal Modalities of CTL and Near Logics." Logical Investigations 21, no. 1 (April 21, 2015): 86–99. http://dx.doi.org/10.21146/2074-1472-2015-21-1-86-99.

Full text

Abstract:

We study an expressive power of temporal operators used in such logics of branching time as computational tree logic or alternating-time temporal logic. To do this we investigate calculi in the first-order language enriched with the temporal operators used in such logics. We show that the resulting languages are so powerful that many ‘natural’ calculi in the languages are not Kripke complete; for example, if a calculus in such language is correct with respect to the class of all serial linear Kripke frames (even just with constant domains) then it is not Kripke complete. Some near questions are discussed.

APA, Harvard, Vancouver, ISO, and other styles

21

Fontaine, Gaëlle, Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Loredana Sorrentino. "Cycle Detection in Computation Tree Logic." Electronic Proceedings in Theoretical Computer Science 226 (September 13, 2016): 164–77. http://dx.doi.org/10.4204/eptcs.226.12.

Full text

APA, Harvard, Vancouver, ISO, and other styles

22

Pan, Haiyu, Yongming Li, Yongzhi Cao, and Zhanyou Ma. "Model checking fuzzy computation tree logic." Fuzzy Sets and Systems 262 (March 2015): 60–77. http://dx.doi.org/10.1016/j.fss.2014.07.008.

Full text

APA, Harvard, Vancouver, ISO, and other styles

23

Fontaine, Gaëlle, Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Loredana Sorrentino. "Cycle detection in computation tree logic." Information and Computation 262 (October 2018): 265–79. http://dx.doi.org/10.1016/j.ic.2018.09.007.

Full text

APA, Harvard, Vancouver, ISO, and other styles

24

Xiong, Liping, and Sumei Guo. "Representation and Reasoning about Strategic Abilities with ω-Regular Properties." Mathematics 9, no. 23 (November 27, 2021): 3052. http://dx.doi.org/10.3390/math9233052.

Full text

Abstract:

Specification and verification of coalitional strategic abilities have been an active research area in multi-agent systems, artificial intelligence, and game theory. Recently, many strategic logics, e.g., Strategy Logic (SL) and alternating-time temporal logic (ATL*), have been proposed based on classical temporal logics, e.g., linear-time temporal logic (LTL) and computational tree logic (CTL*), respectively. However, these logics cannot express general ω-regular properties, the need for which are considered compelling from practical applications, especially in industry. To remedy this problem, in this paper, based on linear dynamic logic (LDL), proposed by Moshe Y. Vardi, we propose LDL-based Strategy Logic (LDL-SL). Interpreted on concurrent game structures, LDL-SL extends SL, which contains existential/universal quantification operators about regular expressions. Here we adopt a branching-time version. This logic can express general ω-regular properties and describe more programmed constraints about individual/group strategies. Then we study three types of fragments (i.e., one-goal, ATL-like, star-free) of LDL-SL. Furthermore, we show that prevalent strategic logics based on LTL/CTL*, such as SL/ATL*, are exactly equivalent with those corresponding star-free strategic logics, where only star-free regular expressions are considered. Moreover, results show that reasoning complexity about the model-checking problems for these new logics, including one-goal and ATL-like fragments, is not harder than those of corresponding SL or ATL*.

APA, Harvard, Vancouver, ISO, and other styles

25

Han, Ying-Jie, Jian-Wei Wang, Chun Huang, and Qing-Lei Zhou. "Computation Tree Logic Formula Model Checking Using DNA Computing." Journal of Nanoelectronics and Optoelectronics 15, no. 5 (May 1, 2020): 620–29. http://dx.doi.org/10.1166/jno.2020.2781.

Full text

Abstract:

Computation tree logic model checking is a formal verification technology that can ensure the correctness of systems. The vast storage density of deoxyribonucleic acid (DNA) molecules and the massive parallelism of DNA computing offer new methods for computation tree logic model checking. In this study, we propose a computation tree logic model checking method based on DNA computing. First, a system to-be-checked and a computation tree logic formula are encoded by single-stranded DNA molecules. Second, these singlestranded DNA molecules are mixed to spontaneously hybridize and form partial or complete double-stranded molecules. Finally, a series of molecular manipulations are applied to detect the double-stranded molecules so that the result whether the system satisfies the computation tree logic formula is obtained. Biological simulations confirm the validity of the new method.

APA, Harvard, Vancouver, ISO, and other styles

26

Calvanese, Diego, Giuseppe De Giacomo, Maurizio Lenzerini, and Moshe Vardi. "Node Selection Query Languages for Trees." Proceedings of the AAAI Conference on Artificial Intelligence 24, no. 1 (July 3, 2010): 279–84. http://dx.doi.org/10.1609/aaai.v24i1.7598.

Full text

Abstract:

The study of node-selection query languages for (finite) trees has been a major topic in the recent research on query lan- guages for Web documents. On one hand, there has been an extensive study of XPath and its various extensions. On the other hand, query languages based on classical logics, such as first-order logic (FO) or monadic second-order logic (MSO), have been considered. Results in this area typically relate an Xpath-based language to a classical logic. What has yet to emerge is an XPath-related language that is expressive as MSO, and at the same time enjoys the computational proper- ties of XPath, which are linear query evaluation and exponen- tial query-containment test. In this paper we propose μXPath, which is the alternation-free fragment of XPath extended with fixpoint operators. Using two-way alternating automata, we show that this language does combine desired expressiveness and computational properties, placing it as an attractive can- didate as the definite query language for trees.

APA, Harvard, Vancouver, ISO, and other styles

27

Reynolds, M. "An axiomatization of full Computation Tree Logic." Journal of Symbolic Logic 66, no. 3 (September 2001): 1011–57. http://dx.doi.org/10.2307/2695091.

Full text

APA, Harvard, Vancouver, ISO, and other styles

28

FERREIRA, FERNANDO. "A NEW COMPUTATION OF THE Σ-ORDINAL OF KPω." Journal of Symbolic Logic 79, no. 01 (March 2014): 306–24. http://dx.doi.org/10.1017/jsl.2013.31.

Full text

Abstract:

Abstract We define a functional interpretation of KP ω using Howard’s primitive recursive tree functionals of finite type and associated terms. We prove that the Σ-ordinal of KP ω is the least ordinal not given by a closed term of the ground type of the trees (the Bachmann-Howard ordinal). We also extend KP ω to a second-order theory with Δ 1-comprehension and strict- ${\rm{\Pi }}_1^1$ reflection and show that the Σ-ordinal of this theory is still the Bachmann-Howard ordinal. It is also argued that the second-order theory is Σ1-conservative over KPω.

APA, Harvard, Vancouver, ISO, and other styles

29

Dasgupta, Pallab, P. P. Chakrabarti, and Jatindra Kumar Deka. "Min-max event-triggered computation tree logic." Sadhana 27, no. 2 (April 2002): 163–80. http://dx.doi.org/10.1007/bf02717182.

Full text

APA, Harvard, Vancouver, ISO, and other styles

30

Ma, Zhanyou, Zhaokai Li, Weijun Li, Yingnan Gao, and Xia Li. "Model Checking Fuzzy Computation Tree Logic Based on Fuzzy Decision Processes with Cost." Entropy 24, no. 9 (August 24, 2022): 1183. http://dx.doi.org/10.3390/e24091183.

Full text

Abstract:

In order to solve the problems in fuzzy computation tree logic model checking with cost operator, we propose a fuzzy decision process computation tree logic model checking method with cost. Firstly, we introduce a fuzzy decision process model with cost, which can not only describe the uncertain choice and transition possibility of systems, but also quantitatively describe the cost of the systems. Secondly, under the model of the fuzzy decision process with cost, we give the syntax and semantics of the fuzzy computation tree logic with cost operators. Thirdly, we study the problem of computation tree logic model checking for fuzzy decision process with cost, and give its matrix calculation method and algorithm. We use the example of medical expert systems to illustrate the method and model checking algorithm.

APA, Harvard, Vancouver, ISO, and other styles

31

Soares Passos, Lígia Maria, and Stéphane Julia. "Linear Logic as a Tool for Qualitative and Quantitative Analysis of Workow Processes." International Journal on Artificial Intelligence Tools 25, no. 03 (June 2016): 1650008. http://dx.doi.org/10.1142/s0218213016500081.

Full text

Abstract:

This article presents a method for qualitative and quantitative analysis of WorkFlow nets based on the proof trees of Linear Logic. The qualitative analysis is concerned with the proof of Soundness correctness criterion defined for WorkFlow nets. To prove the Soundness property, a proof tree of Linear Logic is built for each different scenario of the WorkFlow net. The quantitative analysis is concerned with the resource planning for each task of the workflow process and is based on the computation of symbolic date intervals for task execution. In particular, such symbolic date intervals are computed using the proof trees used to prove Soundness property.

APA, Harvard, Vancouver, ISO, and other styles

32

Zhang, Lan, Ullrich Hustadt, and Clare Dixon. "CTL-RP: A computation tree logic resolution prover." AI Communications 23, no. 2-3 (2010): 111–36. http://dx.doi.org/10.3233/aic-2010-0463.

Full text

APA, Harvard, Vancouver, ISO, and other styles

33

ZHOU, Cong-Hua, Zhi-Feng LIU, and Chang-Da WANG. "Bounded Model Checking for Probabilistic Computation Tree Logic." Journal of Software 23, no. 7 (September 7, 2012): 1656–68. http://dx.doi.org/10.3724/sp.j.1001.2012.04089.

Full text

APA, Harvard, Vancouver, ISO, and other styles

34

Pan, Haiyu, Yongming Li, Yongzhi Cao, and Zhanyou Ma. "Model checking computation tree logic over finite lattices." Theoretical Computer Science 612 (January 2016): 45–62. http://dx.doi.org/10.1016/j.tcs.2015.10.014.

Full text

APA, Harvard, Vancouver, ISO, and other styles

35

Japaridze, Giorgi, and Bikal Lamichhane. "Cirquent Calculus in a Nutshell." Logical Investigations 28, no. 1 (June 26, 2022): 125–41. http://dx.doi.org/10.21146/2074-1472-2022-28-1-125-141.

Full text

Abstract:

This paper is a brief presentation of cirquent calculus, a novel proof system for resource-conscious logics. As such, it is a refinement of sequent calculus with mechanisms that allow to explicitly account for the possibility of sharing of subexpressions/subresources between different expressions/resources. This is achieved by dealing with circuit-style constructs, termed cirquents, instead of formulas, sequents or other tree-like structures. The approach exhibits greater expressiveness, flexibility and efficiency compared to the more traditional proof-theoretic approaches. The need for substantially new deductive tools that could overcome the limitations of sequent calculus while dealing with resource logics surfaced with the birth of computability logic, a game-semantically conceived logic of computational resources and tasks, acting as a formal theory of computability in the same sense as classical logic is a formal theory of truth.Cirquent calculus offers elegant axiomatizations for certain basic fragments of computability logic that have been shown to be inherently unaxiomatizable in sequent calculus or other traditional systems. The paper provides an iformal account on the main characteristic features of cirquent calculus, motivations for it, semantics, advantages over sequent calculus, as well as how cirquent calculus relates to classical and linear logics. Out of several existing cirquent calculus systems, only the simplest and most basic one, CL5, is presented in full detail.

APA, Harvard, Vancouver, ISO, and other styles

36

Ghosh, Krishnendu, and John Schlipf. "Formal modeling of a system of chemical reactions under uncertainty." Journal of Bioinformatics and Computational Biology 12, no. 05 (October 2014): 1440002. http://dx.doi.org/10.1142/s0219720014400022.

Full text

Abstract:

We describe a novel formalism representing a system of chemical reactions, with imprecise rates of reactions and concentrations of chemicals, and describe a model reduction method, pruning, based on the chemical properties. We present two algorithms, midpoint approximation and interval approximation, for construction of efficient model abstractions with uncertainty in data. We evaluate computational feasibility by posing queries in computation tree logic (CTL) on a prototype of extracellular-signal-regulated kinase (ERK) pathway.

APA, Harvard, Vancouver, ISO, and other styles

37

Curcin, Vasa, Moustafa M. Ghanem, and Yike Guo. "Analysing scientific workflows with Computational Tree Logic." Cluster Computing 12, no. 4 (August 19, 2009): 399–419. http://dx.doi.org/10.1007/s10586-009-0099-6.

Full text

APA, Harvard, Vancouver, ISO, and other styles

38

DEL BIMBO, A., and E. VICARIO. "A Visual Formalism for Computational Tree Logic." Journal of Visual Languages & Computing 10, no. 2 (April 1999): 165–87. http://dx.doi.org/10.1006/jvlc.1998.0108.

Full text

APA, Harvard, Vancouver, ISO, and other styles

39

Li, Yongming, Yali Li, and Zhanyou Ma. "Computation tree logic model checking based on possibility measures." Fuzzy Sets and Systems 262 (March 2015): 44–59. http://dx.doi.org/10.1016/j.fss.2014.03.009.

Full text

APA, Harvard, Vancouver, ISO, and other styles

40

Beauquier, Danièle, and Anatol Slissenko. "Polytime model checking for timed probabilistic computation tree logic." Acta Informatica 35, no. 8 (August 1, 1998): 645–64. http://dx.doi.org/10.1007/s002360050136.

Full text

APA, Harvard, Vancouver, ISO, and other styles

41

Huth, Michael. "On finite-state approximants for probabilistic computation tree logic." Theoretical Computer Science 346, no. 1 (November 2005): 113–34. http://dx.doi.org/10.1016/j.tcs.2005.08.008.

Full text

APA, Harvard, Vancouver, ISO, and other styles

42

Gebser, Martin, Tomi Janhunen, and Jussi Rintanen. "Declarative encodings of acyclicity properties." Journal of Logic and Computation 30, no. 4 (September 8, 2015): 923–52. http://dx.doi.org/10.1093/logcom/exv063.

Full text

Abstract:

Abstract Many knowledge representation tasks involve trees or similar structures as abstract datatypes. However, devising compact and efficient declarative representations of such structural properties is non-obvious and can be challenging indeed. In this article, we take a number of acyclicity properties into consideration and investigate various logic-based approaches to encode them. We use answer set programming as the primary representation language but also consider mappings to related formalisms, such as propositional logic, difference logic and linear programming. We study the compactness of encodings and the resulting computational performance on benchmarks involving acyclic or tree structures.

APA, Harvard, Vancouver, ISO, and other styles

43

Zhang, Xin Xing, Qiu Yan Zhu, Jiao Yang Lu, Fu Rui Zhang, Wei Tao Huang, Xue Zhi Ding, and Li Qiu Xia. "The Boolean logic tree of molecular self-assembly system based on cobalt oxyhydroxide nanoflakes for three-state logic computation, sensing and imaging of pyrophosphate in living cells and in vivo." Analyst 144, no. 1 (2019): 274–83. http://dx.doi.org/10.1039/c8an01565a.

Full text

APA, Harvard, Vancouver, ISO, and other styles

44

CARDELLI, LUCA, and GIORGIO GHELLI. "TQL: a query language for semistructured data based on the ambient logic." Mathematical Structures in Computer Science 14, no. 3 (May 20, 2004): 285–327. http://dx.doi.org/10.1017/s0960129504004141.

Full text

Abstract:

The ambient logic is a modal logic that was proposed for the description of the structural and computational properties of distributed and mobile computation. The structural part of the ambient logic is, essentially, a logic of labelled trees, hence it turns out to be a good foundation for query languages for semistructured data, much in the same way as first-order logic is a fitting foundation for relational query languages. We define here a query language for semistructured data that is based on the ambient logic, and we outline an execution model for this language. The language turns out to be quite expressive. Its strong foundations and the equivalences that hold in the ambient logic are helpful in the definition of the language semantics and execution model.

APA, Harvard, Vancouver, ISO, and other styles

45

DI SCIASCIO, EUGENIO, FRANCESCO M. DONINI, and MARINA MONGIELLO. "USING COMPUTATION TREE LOGIC FOR INTELLIGENT INFORMATION SEARCH ON THE WEB." International Journal of Computational Intelligence and Applications 02, no. 03 (September 2002): 245–53. http://dx.doi.org/10.1142/s1469026802000579.

Full text

Abstract:

Web engines crawl hyperlinks to search for new documents; yet when they index discovered documents they basically revert to conventional information retrieval models and concentrate on the indexing of terms in a single document. We propose to overcome such limits with an approach based on temporal logic. By modeling a web site as a finite state transition system we are able to define complex and selective queries over hyperlinks with the aid of Computation Tree Logic operators. We deployed the proposed approach in a prototype system that allows users pose queries in natural language. Queries are automatically translated in Computation Tree Logic, and the answer returned by our system is a set of paths. Experiments carried out with the aid of human experts show improved retrieval effectiveness with respect to current search engines.

APA, Harvard, Vancouver, ISO, and other styles

46

Au, Tsz-Chiu. "Extended Goal Recognition Design with First-Order Computation Tree Logic." Proceedings of the AAAI Conference on Artificial Intelligence 36, no. 9 (June 28, 2022): 9661–68. http://dx.doi.org/10.1609/aaai.v36i9.21200.

Full text

Abstract:

Goal recognition design (GRD) is the task of modifying environments for aiding observers to recognize the objectives of agents during online observations. The worst case distinctiveness (WCD), a widely used performance measure in GRD research, can fail to provide useful guidance to the redesign process when some goals are too hard to be distinguished. Moreover, the existing WCD-based approaches do not work when an agent aims for a sequence of goals instead of just one goal. The paper presents a new GRD framework called extended goal recognition design (EGRD) for goal recognition that involves multiple goals. The objective of EGRD is to modify an environment to minimize the worst case distinctiveness of a goal condition that describes how an agent can reach a set of goals. A goal condition can be formally expressed in first-order computation tree logic (FO-CTL) that can be evaluated by model checking. We introduce a novel graphical representation of FO-CTL sentences that is suitable for extended goal recognition. Moreover, we present a search algorithm for EGRD with a novel caching mechanism. Our experimental results show that the caching mechanism can greatly speed up our EGRD search algorithm by reusing the previous evaluation of FO-CTL sentences.

APA, Harvard, Vancouver, ISO, and other styles

47

Bolotov, Alexander, and Artie Basukoski. "A clausal resolution method for extended computation tree logic ECTL." Journal of Applied Logic 4, no. 2 (June 2006): 141–67. http://dx.doi.org/10.1016/j.jal.2005.06.003.

Full text

APA, Harvard, Vancouver, ISO, and other styles

48

Murano, Aniello, Mimmo Parente, Sasha Rubin, and Loredana Sorrentino. "Model-checking graded computation-tree logic with finite path semantics." Theoretical Computer Science 806 (February 2020): 577–86. http://dx.doi.org/10.1016/j.tcs.2019.09.021.

Full text

APA, Harvard, Vancouver, ISO, and other styles

49

Lück, Martin. "Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic." International Journal of Foundations of Computer Science 29, no. 01 (January 2018): 17–61. http://dx.doi.org/10.1142/s0129054118500028.

Full text

Abstract:

The satisfiability problem of the branching time logic CTL is studied in terms of computational complexity. Tight upper and lower bounds are provided for each temporal operator fragment. In parallel, the minimal model size is studied with a suitable notion of minimality. Thirdly, flat CTL is investigated, i.e., formulas with very low temporal operator nesting depth. A sharp dichotomy is shown in terms of complexity and minimal models: Temporal depth one has low expressive power, while temporal depth two is equivalent to full CTL.

APA, Harvard, Vancouver, ISO, and other styles

50

Meolic, Robert, Tatjana Kapus, and Zmago Brezočnik. "ACTLW – An action-based computation tree logic with unless operator." Information Sciences 178, no. 6 (March 2008): 1542–57. http://dx.doi.org/10.1016/j.ins.2007.10.023.

Full text

APA, Harvard, Vancouver, ISO, and other styles

We offer discounts on all premium plans for authors whose works are included in thematic literature selections. Contact us to get a unique promo code!