Bibliographies thématiques / Linear-time Temporal Logic / Articles de revues

Articles de revues sur le sujet « Linear-time Temporal Logic »

Pour voir les autres types de publications sur ce sujet consultez le lien suivant : Linear-time Temporal Logic.
Auteur : Grafiati
Publié le 11 mars 2023

Créez une référence correcte selon les styles APA, MLA, Chicago, Harvard et plusieurs autres

Choisissez une source :

Consultez les 50 meilleurs articles de revues pour votre recherche sur le sujet « Linear-time Temporal Logic ».

À côté de chaque source dans la liste de références il y a un bouton « Ajouter à la bibliographie ». Cliquez sur ce bouton, et nous générerons automatiquement la référence bibliographique pour la source choisie selon votre style de citation préféré : APA, MLA, Harvard, Vancouver, Chicago, etc.

Vous pouvez aussi télécharger le texte intégral de la publication scolaire au format pdf et consulter son résumé en ligne lorsque ces informations sont inclues dans les métadonnées.

Parcourez les articles de revues sur diverses disciplines et organisez correctement votre bibliographie.

1

Henriksen, Jesper G., et P. S. Thiagarajan. « Dynamic linear time temporal logic ». Annals of Pure and Applied Logic 96, no 1-3 (mars 1999) : 187–207. http://dx.doi.org/10.1016/s0168-0072(98)00039-6.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
2

Wansing, Heinrich, et Norihiro Kamide. « Synchronized Linear-Time Temporal Logic ». Studia Logica 99, no 1-3 (31 août 2011) : 365–88. http://dx.doi.org/10.1007/s11225-011-9357-8.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
3

Kamide, Norihiro, et Heinrich Wansing. « A Paraconsistent Linear-time Temporal Logic ». Fundamenta Informaticae 106, no 1 (2011) : 1–23. http://dx.doi.org/10.3233/fi-2011-374.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
4

Frigeri, Achille, Liliana Pasquale et Paola Spoletini. « Fuzzy Time in Linear Temporal Logic ». ACM Transactions on Computational Logic 15, no 4 (août 2014) : 1–22. http://dx.doi.org/10.1145/2629606.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
5

INDRZEJCZAK, ANDRZEJ. « LINEAR TIME IN HYPERSEQUENT FRAMEWORK ». Bulletin of Symbolic Logic 22, no 1 (mars 2016) : 121–44. http://dx.doi.org/10.1017/bsl.2016.2.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
6

Giero, Mariusz. « The Axiomatization of Propositional Linear Time Temporal Logic ». Formalized Mathematics 19, no 2 (1 janvier 2011) : 113–19. http://dx.doi.org/10.2478/v10037-011-0018-1.

Texte intégral
Résumé :
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].
Styles APA, Harvard, Vancouver, ISO, etc.
7

Shi, Jianqi, Jiawen Xiong et Yanhong Huang. « General past-time linear temporal logic specification mining ». CCF Transactions on High Performance Computing 3, no 4 (19 octobre 2021) : 393–406. http://dx.doi.org/10.1007/s42514-021-00079-4.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
8

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

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
9

Fisher, Michael. « A model checker for linear time temporal logic ». Formal Aspects of Computing 4, no 3 (mai 1992) : 299–319. http://dx.doi.org/10.1007/bf01212306.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
10

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

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
11

Giero, Mariusz. « Weak Completeness Theorem for Propositional Linear Time Temporal Logic ». Formalized Mathematics 20, no 3 (1 décembre 2012) : 227–34. http://dx.doi.org/10.2478/v10037-012-0027-8.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
12

Kröger, Fred, et Stephan Merz. « Temporal Logic and Recursion ». Fundamenta Informaticae 14, no 2 (1 février 1991) : 261–81. http://dx.doi.org/10.3233/fi-1991-14207.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
13

Huang, Samuel, et Rance Cleaveland. « A tableau construction for finite linear-time temporal logic ». Journal of Logical and Algebraic Methods in Programming 125 (février 2022) : 100743. http://dx.doi.org/10.1016/j.jlamp.2021.100743.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
14

Giordano, L. « Reasoning about actions in dynamic linear time temporal logic ». Logic Journal of IGPL 9, no 2 (1 mars 2001) : 273–88. http://dx.doi.org/10.1093/jigpal/9.2.273.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
15

Kamide, Norihiro, et Heinrich Wansing. « Combining linear-time temporal logic with constructiveness and paraconsistency ». Journal of Applied Logic 8, no 1 (mars 2010) : 33–61. http://dx.doi.org/10.1016/j.jal.2009.06.001.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
16

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

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
17

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

Texte intégral
Résumé :
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*.
Styles APA, Harvard, Vancouver, ISO, etc.
18

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

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
19

Kaneiwa, Ken, et Norihiro Kamide. « SEQUENCE-INDEXED LINEAR-TIME TEMPORAL LOGIC : PROOF SYSTEM AND APPLICATION ». Applied Artificial Intelligence 24, no 10 (30 novembre 2010) : 896–913. http://dx.doi.org/10.1080/08839514.2010.514231.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
20

Kojima, Kensuke, et Atsushi Igarashi. « Constructive linear-time temporal logic : Proof systems and Kripke semantics ». Information and Computation 209, no 12 (décembre 2011) : 1491–503. http://dx.doi.org/10.1016/j.ic.2010.09.008.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
21

Torfah, Hazem, et Martin Zimmermann. « The complexity of counting models of linear-time temporal logic ». Acta Informatica 55, no 3 (17 novembre 2016) : 191–212. http://dx.doi.org/10.1007/s00236-016-0284-z.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
22

Thiagarajan, P. S., et I. Walukiewicz. « An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces ». Information and Computation 179, no 2 (décembre 2002) : 230–49. http://dx.doi.org/10.1006/inco.2001.2956.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
23

Giordano, Laura, et Alberto Martelli. « Tableau-based automata construction for dynamic linear time temporal logic* ». Annals of Mathematics and Artificial Intelligence 46, no 3 (mars 2006) : 289–315. http://dx.doi.org/10.1007/s10472-006-9020-7.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
24

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

Texte intégral
Résumé :
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.
Styles 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, no 3-4 (janvier 2006) : 311–47. http://dx.doi.org/10.3166/jancl.16.311-347.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
26

von KARGER, BURGHARD. « Temporal algebra ». Mathematical Structures in Computer Science 8, no 3 (juin 1998) : 277–320. http://dx.doi.org/10.1017/s0960129598002540.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
27

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

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
28

GIORDANO, LAURA, ALBERTO MARTELLI et DANIELE THESEIDER DUPRÉ. « Reasoning about actions with Temporal Answer Sets ». Theory and Practice of Logic Programming 13, no 2 (25 janvier 2012) : 201–25. http://dx.doi.org/10.1017/s1471068411000639.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
29

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

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
30

CABALAR, PEDRO, MARTÍN DIÉGUEZ, TORSTEN SCHAUB et ANNA SCHUHMANN. « Towards Metric Temporal Answer Set Programming ». Theory and Practice of Logic Programming 20, no 5 (septembre 2020) : 783–98. http://dx.doi.org/10.1017/s1471068420000307.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
31

KAMIDE, NORIHIRO. « Embedding theorems for LTL and its variants ». Mathematical Structures in Computer Science 25, no 1 (2 décembre 2014) : 83–134. http://dx.doi.org/10.1017/s0960129514000048.

Texte intégral
Résumé :
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).
Styles APA, Harvard, Vancouver, ISO, etc.
32

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

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
33

Reynolds, Mark. « Axiomatising first-order temporal logic : Until and since over linear time ». Studia Logica 57, no 2-3 (octobre 1996) : 279–302. http://dx.doi.org/10.1007/bf00370836.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
34

Gnatenko, Anton Romanovich, et 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, no 4 (18 décembre 2021) : 356–71. http://dx.doi.org/10.18255/1818-1015-2021-4-356-371.

Texte intégral
Résumé :
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.
Styles 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, no 7 (27 février 2017) : 2271–301. http://dx.doi.org/10.1093/logcom/exx006.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
36

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

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
37

CABALAR, PEDRO, MARTÍN DIÉGUEZ et CONCEPCIÓN VIDAL. « An infinitary encoding of temporal equilibrium logic ». Theory and Practice of Logic Programming 15, no 4-5 (juillet 2015) : 666–80. http://dx.doi.org/10.1017/s1471068415000307.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
38

Jiang, S., et R. Kumar. « Failure Diagnosis of Discrete-Event Systems With Linear-Time Temporal Logic Specifications ». IEEE Transactions on Automatic Control 49, no 6 (juin 2004) : 934–45. http://dx.doi.org/10.1109/tac.2004.829616.

Texte intégral
Styles 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, no 2 (mars 2003) : 393–426. http://dx.doi.org/10.1016/s0022-0000(03)00005-9.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
40

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

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
41

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

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
42

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

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
43

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

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
44

TAKAHASHI, Satoshi, Toshimitsu USHIO et 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, no 9 (2006) : 350–57. http://dx.doi.org/10.5687/iscie.19.350.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
45

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

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
46

DEMRI, STÉPHANE, et DAVID NOWAK. « REASONING ABOUT TRANSFINITE SEQUENCES ». International Journal of Foundations of Computer Science 18, no 01 (février 2007) : 87–112. http://dx.doi.org/10.1142/s0129054107004589.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
47

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

Texte intégral
Résumé :
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.
Styles 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 décembre 2021) : 158–80. http://dx.doi.org/10.5195/bsj.2021.253.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
49

Wolter, Frank, et Michael Zakharyaschev. « A logic for metric and topology ». Journal of Symbolic Logic 70, no 3 (septembre 2005) : 795–828. http://dx.doi.org/10.2178/jsl/1122038915.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
50

Hustadt, Ullrich, Ana Ozaki et Clare Dixon. « Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via Translations ». Journal of Automated Reasoning 64, no 8 (19 février 2020) : 1553–610. http://dx.doi.org/10.1007/s10817-020-09541-4.

Texte intégral
Résumé :
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.
Styles APA, Harvard, Vancouver, ISO, etc.
Nous offrons des réductions sur tous les plans premium pour les auteurs dont les œuvres sont incluses dans des sélections littéraires thématiques. Contactez-nous pour obtenir un code promo unique!

Vers la bibliographie