Acceder

Bibliografías temáticas / Linear-time Temporal Logic / Artículos de revistas

Siga este enlace para ver otros tipos de publicaciones sobre el tema: Linear-time Temporal Logic.

Artículos de revistas sobre el tema "Linear-time Temporal Logic"

Autor: Grafiati

Publicado: 11 de marzo de 2023

Crea una cita precisa en los estilos APA, MLA, Chicago, Harvard y otros

Elija tipo de fuente:

Consulte los 50 mejores artículos de revistas para su investigación sobre el tema "Linear-time Temporal Logic".

Junto a cada fuente en la lista de referencias hay un botón "Agregar a la bibliografía". Pulsa este botón, y generaremos automáticamente la referencia bibliográfica para la obra elegida en el estilo de cita que necesites: APA, MLA, Harvard, Vancouver, Chicago, etc.

También puede descargar el texto completo de la publicación académica en formato pdf y leer en línea su resumen siempre que esté disponible en los metadatos.

Explore artículos de revistas sobre una amplia variedad de disciplinas y organice su bibliografía correctamente.

1

Henriksen, Jesper G. y P. S. Thiagarajan. "Dynamic linear time temporal logic". Annals of Pure and Applied Logic 96, n.º 1-3 (marzo de 1999): 187–207. http://dx.doi.org/10.1016/s0168-0072(98)00039-6.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

2

Wansing, Heinrich y Norihiro Kamide. "Synchronized Linear-Time Temporal Logic". Studia Logica 99, n.º 1-3 (31 de agosto de 2011): 365–88. http://dx.doi.org/10.1007/s11225-011-9357-8.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

3

Kamide, Norihiro y Heinrich Wansing. "A Paraconsistent Linear-time Temporal Logic". Fundamenta Informaticae 106, n.º 1 (2011): 1–23. http://dx.doi.org/10.3233/fi-2011-374.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

4

Frigeri, Achille, Liliana Pasquale y Paola Spoletini. "Fuzzy Time in Linear Temporal Logic". ACM Transactions on Computational Logic 15, n.º 4 (agosto de 2014): 1–22. http://dx.doi.org/10.1145/2629606.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

5

INDRZEJCZAK, ANDRZEJ. "LINEAR TIME IN HYPERSEQUENT FRAMEWORK". Bulletin of Symbolic Logic 22, n.º 1 (marzo de 2016): 121–44. http://dx.doi.org/10.1017/bsl.2016.2.

Texto completo

Resumen

AbstractHypersequent calculus (HC), developed by A. Avron, is one of the most interesting proof systems suitable for nonclassical logics. Although HC has rather simple form, it increases significantly the expressive power of standard sequent calculi (SC). In particular, HC proved to be very useful in the field of proof theory of various nonclassical logics. It may seem surprising that it was not applied to temporal logics so far. In what follows, we discuss different approaches to formalization of logics of linear frames and provide a cut-free HC formalization ofKt4.3, the minimal temporal logic of linear frames, and some of its extensions. The novelty of our approach is that hypersequents are defined not as finite (multi)sets but as finite lists of ordinary sequents. Such a solution allows both linearity of time flow, and symmetry of past and future, to be incorporated by means of six temporal rules (three for future-necessity and three dual rules for past-necessity). Extensions of the basic calculus with simple structural rules cover logics of serial and dense frames. Completeness is proved by Schütte/Hintikka-style argument using models built from saturated hypersequents.

Los estilos APA, Harvard, Vancouver, ISO, etc.

6

Giero, Mariusz. "The Axiomatization of Propositional Linear Time Temporal Logic". Formalized Mathematics 19, n.º 2 (1 de enero de 2011): 113–19. http://dx.doi.org/10.2478/v10037-011-0018-1.

Texto completo

Resumen

The Axiomatization of Propositional Linear Time Temporal Logic The article introduces propositional linear time temporal logic as a formal system. Axioms and rules of derivation are defined. Soundness Theorem and Deduction Theorem are proved [9].

Los estilos APA, Harvard, Vancouver, ISO, etc.

7

Shi, Jianqi, Jiawen Xiong y Yanhong Huang. "General past-time linear temporal logic specification mining". CCF Transactions on High Performance Computing 3, n.º 4 (19 de octubre de 2021): 393–406. http://dx.doi.org/10.1007/s42514-021-00079-4.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

8

Tonetta, Stefano. "Linear-time Temporal Logic with Event Freezing Functions". Electronic Proceedings in Theoretical Computer Science 256 (6 de septiembre de 2017): 195–209. http://dx.doi.org/10.4204/eptcs.256.14.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

9

Fisher, Michael. "A model checker for linear time temporal logic". Formal Aspects of Computing 4, n.º 3 (mayo de 1992): 299–319. http://dx.doi.org/10.1007/bf01212306.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

10

Jonsson, Bengt y Tsay Yih-Kuen. "Assumption/guarantee specifications in linear-time temporal logic". Theoretical Computer Science 167, n.º 1-2 (1996): 47–72. http://dx.doi.org/10.1016/0304-3975(96)00069-2.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

11

Giero, Mariusz. "Weak Completeness Theorem for Propositional Linear Time Temporal Logic". Formalized Mathematics 20, n.º 3 (1 de diciembre de 2012): 227–34. http://dx.doi.org/10.2478/v10037-012-0027-8.

Texto completo

Resumen

Summary We prove weak (finite set of premises) completeness theorem for extended propositional linear time temporal logic with irreflexive version of until-operator. We base it on the proof of completeness for basic propositional linear time temporal logic given in [20] which roughly follows the idea of the Henkin-Hasenjaeger method for classical logic. We show that a temporal model exists for every formula which negation is not derivable (Satisfiability Theorem). The contrapositive of that theorem leads to derivability of every valid formula. We build a tree of consistent and complete PNPs which is used to construct the model.

Los estilos APA, Harvard, Vancouver, ISO, etc.

12

Kröger, Fred y Stephan Merz. "Temporal Logic and Recursion". Fundamenta Informaticae 14, n.º 2 (1 de febrero de 1991): 261–81. http://dx.doi.org/10.3233/fi-1991-14207.

Texto completo

Resumen

We propose a temporal logic based on structures divided into several layers of linear “time scales” and give a sound and complete derivation system. The logic is applied to the formulation and verification of assertions about sequential recursive programs.

Los estilos APA, Harvard, Vancouver, ISO, etc.

13

Huang, Samuel y Rance Cleaveland. "A tableau construction for finite linear-time temporal logic". Journal of Logical and Algebraic Methods in Programming 125 (febrero de 2022): 100743. http://dx.doi.org/10.1016/j.jlamp.2021.100743.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

14

Giordano, L. "Reasoning about actions in dynamic linear time temporal logic". Logic Journal of IGPL 9, n.º 2 (1 de marzo de 2001): 273–88. http://dx.doi.org/10.1093/jigpal/9.2.273.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

15

Kamide, Norihiro y Heinrich Wansing. "Combining linear-time temporal logic with constructiveness and paraconsistency". Journal of Applied Logic 8, n.º 1 (marzo de 2010): 33–61. http://dx.doi.org/10.1016/j.jal.2009.06.001.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

16

Kamide, Norihiro. "Bounded linear-time temporal logic: A proof-theoretic investigation". Annals of Pure and Applied Logic 163, n.º 4 (abril de 2012): 439–66. http://dx.doi.org/10.1016/j.apal.2011.12.002.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

17

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

Texto completo

Resumen

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

Los estilos APA, Harvard, Vancouver, ISO, etc.

18

AGUADO, FELICIDAD, PEDRO CABALAR, GILBERTO PÉREZ, CONCEPCIÓN VIDAL y MARTÍN DIÉGUEZ. "Temporal logic programs with variables". Theory and Practice of Logic Programming 17, n.º 2 (11 de noviembre de 2016): 226–43. http://dx.doi.org/10.1017/s1471068416000570.

Texto completo

Resumen

AbstractIn this note, we consider the problem of introducing variables in temporal logic programs under the formalism of Temporal Equilibrium Logic, an extension of Answer Set Programming for dealing with linear-time modal operators. To this aim, we provide a definition of a first-order version of Temporal Equilibrium Logic that shares the syntax of first-order Linear-time Temporal Logic but has different semantics, selecting some Linear-time Temporal Logic models we call temporal stable models. Then, we consider a subclass of theories (called splittable temporal logic programs) that are close to usual logic programs but allowing a restricted use of temporal operators. In this setting, we provide a syntactic definition of safe variables that suffices to show the property of domain independence – that is, addition of arbitrary elements in the universe does not vary the set of temporal stable models. Finally, we present a method for computing the derivable facts by constructing a non-temporal logic program with variables that is fed to a standard Answer Set Programming grounder. The information provided by the grounder is then used to generate a subset of ground temporal rules which is equivalent to (and generally smaller than) the full program instantiation.

Los estilos APA, Harvard, Vancouver, ISO, etc.

19

Kaneiwa, Ken y Norihiro Kamide. "SEQUENCE-INDEXED LINEAR-TIME TEMPORAL LOGIC: PROOF SYSTEM AND APPLICATION". Applied Artificial Intelligence 24, n.º 10 (30 de noviembre de 2010): 896–913. http://dx.doi.org/10.1080/08839514.2010.514231.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

20

Kojima, Kensuke y Atsushi Igarashi. "Constructive linear-time temporal logic: Proof systems and Kripke semantics". Information and Computation 209, n.º 12 (diciembre de 2011): 1491–503. http://dx.doi.org/10.1016/j.ic.2010.09.008.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

21

Torfah, Hazem y Martin Zimmermann. "The complexity of counting models of linear-time temporal logic". Acta Informatica 55, n.º 3 (17 de noviembre de 2016): 191–212. http://dx.doi.org/10.1007/s00236-016-0284-z.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

22

Thiagarajan, P. S. y I. Walukiewicz. "An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces". Information and Computation 179, n.º 2 (diciembre de 2002): 230–49. http://dx.doi.org/10.1006/inco.2001.2956.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

23

Giordano, Laura y Alberto Martelli. "Tableau-based automata construction for dynamic linear time temporal logic*". Annals of Mathematics and Artificial Intelligence 46, n.º 3 (marzo de 2006): 289–315. http://dx.doi.org/10.1007/s10472-006-9020-7.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

24

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

Texto completo

Resumen

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.

Los estilos APA, Harvard, Vancouver, ISO, etc.

25

Demri, Stéphane. "Linear-time temporal logics with Presburger constraints: an overview ★". Journal of Applied Non-Classical Logics 16, n.º 3-4 (enero de 2006): 311–47. http://dx.doi.org/10.3166/jancl.16.311-347.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

26

von KARGER, BURGHARD. "Temporal algebra". Mathematical Structures in Computer Science 8, n.º 3 (junio de 1998): 277–320. http://dx.doi.org/10.1017/s0960129598002540.

Texto completo

Resumen

We develop temporal logic from the theory of complete lattices, Galois connections and fixed points. In particular, we prove that all seventeen axioms of Manna and Pnueli's sound and complete proof system for linear temporal logic can be derived from just two postulates, namely that ([oplus ], &[ominus ]tilde;) is a Galois connection and that ([ominus ], [oplus ]) is a perfect Galois connection. We also obtain a similar result for the branching time logic CTL.A surprising insight is that most of the theory can be developed without the use of negation. In effect, we are studying intuitionistic temporal logic. Several examples of such structures occurring in computer science are given. Finally, we show temporal algebra at work in the derivation of a simple graph-theoretic algorithm.This paper is tutorial in style and there are no difficult technical results. To the experts in temporal logics, we hope to convey the simplicity and beauty of algebraic reasoning as opposed to the machine-orientedness of logical deduction. To those familiar with the calculational approach to programming, we want to show that their methods extend easily and smoothly to temporal reasoning. For anybody else, this text may serve as a gentle introduction to both areas.

Los estilos APA, Harvard, Vancouver, ISO, etc.

27

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

Texto completo

Resumen

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.

Los estilos APA, Harvard, Vancouver, ISO, etc.

28

GIORDANO, LAURA, ALBERTO MARTELLI y DANIELE THESEIDER DUPRÉ. "Reasoning about actions with Temporal Answer Sets". Theory and Practice of Logic Programming 13, n.º 2 (25 de enero de 2012): 201–25. http://dx.doi.org/10.1017/s1471068411000639.

Texto completo

Resumen

AbstractIn this paper, we combine Answer Set Programming (ASP) with Dynamic Linear Time Temporal Logic (DLTL) to define a temporal logic programming language for reasoning about complex actions and infinite computations. DLTL extends propositional temporal logic of linear time with regular programs of propositional dynamic logic, which are used for indexing temporal modalities. The action language allows general DLTL formulas to be included in domain descriptions to constrain the space of possible extensions. We introduce a notion of Temporal Answer Set for domain descriptions, based on the usual notion of Answer Set. Also, we provide a translation of domain descriptions into standard ASP and use Bounded Model Checking (BMC) techniques for the verification of DLTL constraints.

Los estilos APA, Harvard, Vancouver, ISO, etc.

29

Wen, Zhi Cheng y Zhi Gang Chen. "Extending Linear Temporal Logic with Clocks to Object-Z". Applied Mechanics and Materials 513-517 (febrero de 2014): 927–30. http://dx.doi.org/10.4028/www.scientific.net/amm.513-517.927.

Texto completo

Resumen

Object-Z, an extension to formal specification language Z, is good for describing large scale Object-Oriented software specification. While Object-Z has found application in a number of areas, its utility is limited by its inability to specify continuous variables and real-time constraints. Linear temporal logic can describe real-time system, but it can not deal with time variables well and also can not describe formal specification modularly. This paper extends linear temporal logic with clocks (LTLC) and presents an approach to adding linear temporal logic with clocks to Object-Z. Extended Object-Z with LTLC, a modular formal specification language, is a minimum extension of the syntax and semantics of Object-Z. The main advantage of this extension lies in that it is convenient to describe and verify the complex real-time software specification.

Los estilos APA, Harvard, Vancouver, ISO, etc.

30

CABALAR, PEDRO, MARTÍN DIÉGUEZ, TORSTEN SCHAUB y ANNA SCHUHMANN. "Towards Metric Temporal Answer Set Programming". Theory and Practice of Logic Programming 20, n.º 5 (septiembre de 2020): 783–98. http://dx.doi.org/10.1017/s1471068420000307.

Texto completo

Resumen

AbstractWe elaborate upon the theoretical foundations of a metric temporal extension of Answer Set Programming. In analogy to previous extensions of ASP with constructs from Linear Temporal and Dynamic Logic, we accomplish this in the setting of the logic of Here-and-There and its non-monotonic extension, called Equilibrium Logic. More precisely, we develop our logic on the same semantic underpinnings as its predecessors and thus use a simple time domain of bounded time steps. This allows us to compare all variants in a uniform framework and ultimately combine them in a common implementation.

Los estilos APA, Harvard, Vancouver, ISO, etc.

31

KAMIDE, NORIHIRO. "Embedding theorems for LTL and its variants". Mathematical Structures in Computer Science 25, n.º 1 (2 de diciembre de 2014): 83–134. http://dx.doi.org/10.1017/s0960129514000048.

Texto completo

Resumen

In this paper, we prove some embedding theorems for LTL (linear-time temporal logic) and its variants:viz. some generalisations, extensions and fragments of LTL. Using these embedding theorems, we give uniform proofs of the completeness, cut-elimination and/or decidability theorems for LTL and its variants. The proposed embedding theorems clarify the relationships between some LTL-variations (for example, LTL, a dynamic topological logic, a fixpoint logic, a spatial logic, Prior's logic, Davies' logic and an NP-complete LTL) and some traditional logics (for example, classical logic, intuitionistic logic and infinitary logic).

Los estilos APA, Harvard, Vancouver, ISO, etc.

32

Zanma, Tadanao, Shigeru Aoyama y Muneaki Ishida. "Diagnosis of Discrete Event System with Linear-Time Temporal Logic Proposition". IEEJ Transactions on Electronics, Information and Systems 125, n.º 3 (2005): 486–95. http://dx.doi.org/10.1541/ieejeiss.125.486.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

33

Reynolds, Mark. "Axiomatising first-order temporal logic: Until and since over linear time". Studia Logica 57, n.º 2-3 (octubre de 1996): 279–302. http://dx.doi.org/10.1007/bf00370836.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

34

Gnatenko, Anton Romanovich y Vladimir Anatolyevich Zakharov. "On the Satisfiability and Model Checking for one Parameterized Extension of Linear-time Temporal Logic". Modeling and Analysis of Information Systems 28, n.º 4 (18 de diciembre de 2021): 356–71. http://dx.doi.org/10.18255/1818-1015-2021-4-356-371.

Texto completo

Resumen

Sequential reactive systems are computer programs or hardware devices which process the flows of input data or control signals and output the streams of instructions or responses. When designing such systems one needs formal specification languages capable of expressing the relationships between the input and output flows. Previously, we introduced a family of such specification languages based on temporal logics $LTL$, $CTL$ and $CTL^*$ combined with regular languages. A characteristic feature of these new extensions of conventional temporal logics is that temporal operators and basic predicates are parameterized by regular languages. In our early papers, we estimated the expressive power of the new temporal logic $Reg$-$LTL$ and introduced a model checking algorithm for $Reg$-$LTL$, $Reg$-$CTL$, and $Reg$-$CTL^*$. The main issue which still remains unclear is the complexity of decision problems for these logics. In the paper, we give a complete solution to satisfiability checking and model checking problems for $Reg$-$LTL$ and prove that both problems are Pspace-complete. The computational hardness of the problems under consideration is easily proved by reducing to them the intersection emptyness problem for the families of regular languages. The main result of the paper is an algorithm for reducing the satisfiability of checking $Reg$-$LTL$ formulas to the emptiness problem for Buchi automata of relatively small size and a description of a technique that allows one to check the emptiness of the obtained automata within space polynomial of the size of input formulas.

Los estilos APA, Harvard, Vancouver, ISO, etc.

35

Kamide, Norihiro. "Relating first-order monadic omega-logic, propositional linear-time temporal logic, propositional generalized definitional reflection logic and propositional infinitary logic". Journal of Logic and Computation 27, n.º 7 (27 de febrero de 2017): 2271–301. http://dx.doi.org/10.1093/logcom/exx006.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

36

Chen, Cheng-Chia y I.-Peng Lin. "The computational complexity of satisfiability of temporal Horn formulas in propositional linear-time temporal logic". Information Processing Letters 45, n.º 3 (marzo de 1993): 131–36. http://dx.doi.org/10.1016/0020-0190(93)90014-z.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

37

CABALAR, PEDRO, MARTÍN DIÉGUEZ y CONCEPCIÓN VIDAL. "An infinitary encoding of temporal equilibrium logic". Theory and Practice of Logic Programming 15, n.º 4-5 (julio de 2015): 666–80. http://dx.doi.org/10.1017/s1471068415000307.

Texto completo

Resumen

AbstractThis paper studies the relation between two recent extensions of propositional Equilibrium Logic, a well-known logical characterisation of Answer Set Programming. In particular, we show how Temporal Equilibrium Logic, which introduces modal operators as those typically handled in Linear-Time Temporal Logic (LTL), can be encoded into Infinitary Equilibrium Logic, a recent formalisation that allows the use of infinite conjunctions and disjunctions. We prove the correctness of this encoding and, as an application, we further use it to show that the semantics of the temporal logic programming formalism called TEMPLOG is subsumed by Temporal Equilibrium Logic.

Los estilos APA, Harvard, Vancouver, ISO, etc.

38

Jiang, S. y R. Kumar. "Failure Diagnosis of Discrete-Event Systems With Linear-Time Temporal Logic Specifications". IEEE Transactions on Automatic Control 49, n.º 6 (junio de 2004): 934–45. http://dx.doi.org/10.1109/tac.2004.829616.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

39

Reynolds, M. "The complexity of the temporal logic with “until” over general linear time". Journal of Computer and System Sciences 66, n.º 2 (marzo de 2003): 393–426. http://dx.doi.org/10.1016/s0022-0000(03)00005-9.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

40

Evangelista, S., C. Kaiser, J. F. Pradat-Peyre y P. Rousseau. "Verifying linear time temporal logic properties of concurrent Ada programs with quasar". ACM SIGAda Ada Letters XXIV, n.º 1 (marzo de 2004): 17–24. http://dx.doi.org/10.1145/992211.958424.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

41

Lacerda, Bruno y Pedro Lima. "Linear-time temporal logic control of discrete event models of cooperative robots". Journal of Physical Agents (JoPha) 2, n.º 1 (2008): 53–61. http://dx.doi.org/10.14198/jopha.2008.2.1.05.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

42

Szalas, Andrzej. "A complete axiomatic characterization of first-order temporal logic of linear time". Theoretical Computer Science 54, n.º 2-3 (octubre de 1987): 199–214. http://dx.doi.org/10.1016/0304-3975(87)90129-0.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

43

Dietrich, F., X. Logean y J. P. Hubaux. "Modeling and testing object-oriented distributed systems with linear-time temporal logic". Concurrency and Computation: Practice and Experience 13, n.º 5 (2001): 385–420. http://dx.doi.org/10.1002/cpe.571.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

44

TAKAHASHI, Satoshi, Toshimitsu USHIO y Masakazu ADACHI. "Detection of Automation Surprises for a Manual Modeled by Linear-Time Temporal Logic". Transactions of the Institute of Systems, Control and Information Engineers 19, n.º 9 (2006): 350–57. http://dx.doi.org/10.5687/iscie.19.350.

Texto completo

Los estilos APA, Harvard, Vancouver, ISO, etc.

45

Ito, Sohei, Takuma Ichinose, Masaya Shimakawa, Naoko Izumi, Shigeki Hagihara y Naoki Yonezaki. "Modular analysis of gene networks by linear temporal logic". Journal of Integrative Bioinformatics 10, n.º 2 (1 de junio de 2013): 12–23. http://dx.doi.org/10.1515/jib-2013-216.

Texto completo

Resumen

Summary Despite a lot of advances in biology and genomics, it is still difficult to utilise such valuable knowledge and information to understand and analyse large biological systems due to high computational complexity. In this paper we propose a modular method with which from several small network analyses we analyse a large network by integrating them. This method is based on the qualitative framework proposed by authors in which an analysis of gene networks is reduced to checking satisfiability of linear temporal logic formulae. The problem of linear temporal logic satisfiability checking needs exponential time in the size of a formula. Thus it is difficult to analyse large networks directly in this method since the size of a formula grows linearly to the size of a network. The modular method alleviates this computational difficulty. We show some experimental results and see how we benefit from the modular analysis method.

Los estilos APA, Harvard, Vancouver, ISO, etc.

46

DEMRI, STÉPHANE y DAVID NOWAK. "REASONING ABOUT TRANSFINITE SEQUENCES". International Journal of Foundations of Computer Science 18, n.º 01 (febrero de 2007): 87–112. http://dx.doi.org/10.1142/s0129054107004589.

Texto completo

Resumen

We introduce a family of temporal logics to specify the behavior of systems with Zeno behaviors. We extend linear-time temporal logic LTL to authorize models admitting Zeno sequences of actions and quantitative temporal operators indexed by ordinals replace the standard next-time and until future-time operators. Our aim is to control such systems by designing controllers that safely work on ω-sequences but interact synchronously with the system in order to restrict their behaviors. We show that the satisfiability and model-checking for the logics working on ωk-sequences is EXPSPACE-complete when the integers are represented in binary, and PSPACE-complete with a unary representation. To do so, we substantially extend standard results about LTL by introducing a new class of succinct ordinal automata that can encode the interaction between the different quantitative temporal operators.

Los estilos APA, Harvard, Vancouver, ISO, etc.

47

Ramakrishna, Y. S., L. E. Moser, L. K. Dillon, P. M. Melliar-Smith y G. Kutty. "An Automata-Theoretic Decision Procedure for Propositional Temporal Logic with Since and Until1". Fundamenta Informaticae 17, n.º 3 (1 de septiembre de 1992): 271–82. http://dx.doi.org/10.3233/fi-1992-17307.

Texto completo

Resumen

We present an automata-theoretic decision procedure for Since/Until Temporal Logic (SUTL), a linear-time propositional temporal logic with strong non-strict since and until operators. The logic, which is intended for specifying and reasoning about computer systems, employs neither next nor previous operators. Such operators obstruct the use of hierarchical abstraction and refinement and make reasoning about concurrency difficult. A proof of the soundness and completeness of the decision procedure is given, and its complexity is analyzed.

Los estilos APA, Harvard, Vancouver, ISO, etc.

48

Feldman, Irina Alexandra. "Ruina/basural: Lógicas temporales y espaciales de la ciudad de La Paz en Saenz y Viscarra". Bolivian Studies Journal 26 (10 de diciembre de 2021): 158–80. http://dx.doi.org/10.5195/bsj.2021.253.

Texto completo

Resumen

This article analyzes spatio-temporal logics in the representation of the city of La Paz in Imágenes Paceñas by Jaime Saenz and the urban chronicles of Víctor Hugo Viscarra. Juxtaposing the concepts of chrononormativity and queer time, it explores how linear temporal logic remains insufficient for the understanding of the city and its inhabitants in the two narrative projects. The article postulates that the marginal spaces of architectural ruins and garbage dumps, and the marginalized people who inhabit queer space-time are key to “revealing the hidden city” and understanding its contradictory place in the national narrative and space.

Los estilos APA, Harvard, Vancouver, ISO, etc.

49

Wolter, Frank y Michael Zakharyaschev. "A logic for metric and topology". Journal of Symbolic Logic 70, n.º 3 (septiembre de 2005): 795–828. http://dx.doi.org/10.2178/jsl/1122038915.

Texto completo

Resumen

AbstractWe propose a logic for reasoning about metric spaces with the induced topologies. It combines the ‘qualitative’ interior and closure operators with ‘quantitative’ operators ‘somewhere in the sphere of radius r’ including or excluding the boundary. We supply the logic with both the intended metric space semantics and a natural relational semantics, and show that the latter (i) provides finite partial representations of (in general) infinite metric models and (ii) reduces the standard ‘ε-definitions’ of closure and interior to simple constraints on relations. These features of the relational semantics suggest a finite axiomatisation of the logic and provide means to prove its EXPTIME-completeness (even if the rational numerical parameters are coded in binary). An extension with metric variables satisfying linear rational (in)equalities is proved to be decidable as well. Our logic can be regarded as a ‘well-behaved’ common denominator of logical systems constructed in temporal, spatial, and similarity-based quantitative and qualitative representation and reasoning. Interpreted on the real line (with its Euclidean metric), it is a natural fragment of decidable temporal logics for specification and verification of real-time systems. On the real plane, it is closely related to quantitative and qualitative formalisms for spatial representation and reasoning, but this time the logic becomes undecidable.

Los estilos APA, Harvard, Vancouver, ISO, etc.

50

Hustadt, Ullrich, Ana Ozaki y Clare Dixon. "Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via Translations". Journal of Automated Reasoning 64, n.º 8 (19 de febrero de 2020): 1553–610. http://dx.doi.org/10.1007/s10817-020-09541-4.

Texto completo

Resumen

Abstract We study translations from metric temporal logic (MTL) over the natural numbers to linear temporal logic (LTL). In particular, we present two approaches for translating from MTL to LTL which preserve the complexity of the satisfiability problem for MTL. In each of these approaches we consider the case where the mapping between states and time points is given by (i) a strict monotonic function and by (ii) a non-strict monotonic function (which allows multiple states to be mapped to the same time point). We use this logic to model examples from robotics, traffic management, and scheduling, discussing the effects of different modelling choices. Our translations allow us to utilise LTL solvers to solve satisfiability and we empirically compare the translations, showing in which cases one performs better than the other. We also define a branching-time version of the logic and provide translations into computation tree logic.

Los estilos APA, Harvard, Vancouver, ISO, etc.

Ofrecemos descuentos en todos los planes premium para autores cuyas obras están incluidas en selecciones literarias temáticas. ¡Contáctenos para obtener un código promocional único!