Zaloguj się

Gotowe bibliografie tematyczne / Computation Tree Logics / Artykuły w czasopismach

Kliknij ten link, aby zobaczyć inne rodzaje publikacji na ten temat: Computation Tree Logics.

Artykuły w czasopismach na temat „Computation Tree Logics”

Autor: Grafiati

Data publikacji: 6 września 2023

Data aktualizacji: 7 września 2023

Utwórz poprawne odniesienie w stylach APA, MLA, Chicago, Harvard i wielu innych

Wybierz rodzaj źródła:

Sprawdź 50 najlepszych artykułów w czasopismach naukowych na temat „Computation Tree Logics”.

Przycisk „Dodaj do bibliografii” jest dostępny obok każdej pracy w bibliografii. Użyj go – a my automatycznie utworzymy odniesienie bibliograficzne do wybranej pracy w stylu cytowania, którego potrzebujesz: APA, MLA, Harvard, Chicago, Vancouver itp.

Możesz również pobrać pełny tekst publikacji naukowej w formacie „.pdf” i przeczytać adnotację do pracy online, jeśli odpowiednie parametry są dostępne w metadanych.

Przeglądaj artykuły w czasopismach z różnych dziedzin i twórz odpowiednie bibliografie.

1

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

2

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

3

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

4

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

5

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

6

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

7

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

8

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

9

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

10

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

Pełny tekst źródła

Streszczenie:

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

Style APA, Harvard, Vancouver, ISO itp.

11

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

12

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

13

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

14

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

15

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

16

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

17

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

18

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

19

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

20

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

21

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

22

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

23

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

24

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

Pełny tekst źródła

Streszczenie:

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*.

Style APA, Harvard, Vancouver, ISO itp.

25

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

26

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

27

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

28

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

Pełny tekst źródła

Streszczenie:

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ω.

Style APA, Harvard, Vancouver, ISO itp.

29

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

30

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

31

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

32

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

33

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

34

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

35

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

36

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

37

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

38

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

39

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

40

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

41

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

42

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

43

Zhang, Xin Xing, Qiu Yan Zhu, Jiao Yang Lu, Fu Rui Zhang, Wei Tao Huang, Xue Zhi Ding i 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, nr 1 (2019): 274–83. http://dx.doi.org/10.1039/c8an01565a.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

44

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

45

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

46

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

47

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

48

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

49

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

50

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Oferujemy zniżki na wszystkie plany premium dla autorów, których prace zostały uwzględnione w tematycznych zestawieniach literatury. Skontaktuj się z nami, aby uzyskać unikalny kod promocyjny!