Stem ltl$ (all stems)

102 papers:

TACAS-2015-CiniF #ltl #proving #runtime #verification

An LTL Proof System for Runtime Verification (CC, AF), pp. 581–595.

TACAS-2015-KiniV #automaton #ltl #probability

Limit Deterministic and Probabilistic Automata for LTL ∖ GU (DK, MV), pp. 628–642.

TACAS-2015-MolnarDVB #incremental #induction #ltl #model checking #proving

Saturation-Based Incremental LTL Model Checking with Inductive Proofs (VM, DD, AV, TB), pp. 643–657.

LATA-2015-Salem #automaton #ltl #model checking #testing

Single-Pass Testing Automata for LTL Model Checking (AEBS), pp. 563–576.

FM-2015-DuLT #independence #ltl #monitoring #policy #runtime

Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL (XD, YL, AT), pp. 231–247.

ESEC-FSE-2015-MaozR #ltl #specification #synthesis

GR(1) synthesis for LTL specification patterns (SM, JOR), pp. 96–106.

ICSE-v1-2015-BaresiKR #ltl #performance #scalability #specification #verification

Efficient Scalable Verification of LTL Specifications (LB, MMPK, MR), pp. 711–721.

CAV-2015-DietschHLP #approach #ltl #model checking #modulo theories

Fairness Modulo Theory: A New Approach to LTL Software Model Checking (DD, MH, VL, AP), pp. 49–66.

CAV-2015-FinkbeinerRS #algorithm #model checking

Algorithms for Model Checking HyperLTL and HyperCTL ^* (BF, MNR, CS), pp. 30–48.

FoSSaCS-2014-AlmagorK #synthesis

Latticed-LTL Synthesis in the Presence of Noisy Inputs (SA, OK), pp. 226–241.

TACAS-2014-AlmagorBK #ltl

Discounting in LTL (SA, UB, OK), pp. 424–439.

IFM-2014-SchneiderTWW #ltl #refinement

Managing LTL Properties in Event-B Refinement (SAS, HT, HW, DMW), pp. 221–237.

FSE-2014-LiYP0H #finite #infinity #ltl #named #satisfiability

Aalta: an LTL satisfiability checker over Infinite/Finite traces (JL, YY, GP, LZ, JH), pp. 731–734.

CAV-2014-ChengHRS #automation #generative #named #source code

G4LTL-ST: Automatic Generation of PLC Programs (CHC, CHH, HR, SS), pp. 541–549.

CAV-2014-CimattiGMT #hybrid #ltl #verification

Verifying LTL Properties of Hybrid Systems with K-Liveness (AC, AG, SM, ST), pp. 424–440.

CAV-2014-EsparzaK #approach #automaton #composition #ltl

From LTL to Deterministic Automata: A Safraless Compositional Approach (JE, JK), pp. 192–208.

IJCAR-2014-Gore #fixpoint #logic #ltl

And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL (RG), pp. 26–45.

LICS-CSL-2014-MareticDB #ltl

Anchored LTL separation (GPM, MTD, DAB), p. 9.

VMCAI-2014-KiniV #automaton #ltl #probability #safety #specification

Probabilistic Automata for Safety LTL Specifications (DK, MV), pp. 118–136.

TACAS-2013-BenediktLW #ltl #markov #model checking

LTL Model Checking of Interval Markov Chains (MB, RL, JW), pp. 32–46.

TACAS-2013-BohyBFR #ltl #specification #synthesis

Synthesis from LTL Specifications with Mean-Payoff Objectives (AB, VB, EF, JFR), pp. 169–184.

TACAS-2013-SongT #detection #ltl #model checking

LTL Model-Checking for Malware Detection (FS, TT), pp. 416–431.

QAPL-2013-Schuppan #ltl #satisfiability

Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance (VS), pp. 49–65.

CAV-2013-ChatterjeeGK #automaton #ltl #model checking #probability #synthesis

Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis (KC, AG, JK), pp. 559–575.

CAV-2013-EsparzaLNNSS #execution #ltl #model checking

A Fully Verified Executable LTL Model Checker (JE, PL, RN, TN, AS, JGS), pp. 463–478.

TACAS-2012-BabiakKRS #automaton #ltl #performance

LTL to Büchi Automata Translation: Fast and More Deterministic (TB, MK, VR, JS), pp. 95–109.

CIAA-2012-Mandrali #ltl

Weighted LTL with Discounting (EM), pp. 353–360.

FM-2012-BauerF #distributed #ltl #monitoring

Decentralised LTL Monitoring (AKB, YF), pp. 85–100.

KR-2012-FelliGL #ltl #multi #protocol #specification

Synthesizing Agent Protocols From LTL Specifications Against Multiple Partially-Observable Environments (PF, GDG, AL).

SEKE-2012-SalamahEO #automaton #consistency #ltl #using

Consistency Checks of System Properties Using LTL and Büchi Automata (SS, ME, OO), pp. 39–44.

QAPL-2012-CormieBowinsB #ltl #model checking #probability

Measuring Progress of Probabilistic LTL Model Checking (ECB, FvB), pp. 33–47.

CAV-2012-BohyBFJR #ltl #synthesis

Acacia+, a Tool for LTL Synthesis (AB, VB, EF, NJ, JFR), pp. 652–657.

CAV-2012-Ehlers #ltl #synthesis

ACTL ∩ LTL Synthesis (RE), pp. 39–54.

CAV-2012-KretinskyE #automaton #ltl

Deterministic Automata for the (F, G)-Fragment of LTL (JK, JE), pp. 7–22.

IJCAR-2012-DemriDS #ltl

Taming Past LTL and Flat Counter Systems (SD, AKD, AS), pp. 179–193.

IFM-J-2009-BenesBBCSV11 #automaton #component #ltl #partial order #reduction

Partial order reduction for state/event LTL with application to component-interaction automata (NB, LB, BB, IC, JS, PV), pp. 877–890.

FM-2011-RozierV #approach #encoding #ltl #multi #satisfiability

A Multi-encoding Approach for LTL Symbolic Satisfiability Checking (KYR, MYV), pp. 417–431.

SEFM-2011-MorseCNF #bound #ltl #model checking

Context-Bounded Model Checking of LTL Properties for ANSI-C Software (JM, LCC, DN, BF), pp. 302–317.

CAV-2011-BaeM #ltl #model checking #parametricity

State/Event-Based LTL Model Checking under Parametric Generalized Fairness (KB, JM), pp. 132–148.

FoSSaCS-2010-DemriS #decidability #ltl #model checking

When Model-Checking Freeze LTL over Counter Machines Becomes Decidable (SD, AS), pp. 176–190.

FoSSaCS-2010-ToL #algorithm #decidability #infinity #ltl #model checking

Algorithmic Metatheorems for Decidable LTL Model Checking over Infinite Systems (AWT, LL), pp. 221–236.

SEFM-2010-BersaniCFPR #constraints #integer #ltl #runtime #smt #specification #verification

SMT-based Verification of LTL Specification with Integer Constraints and its Application to Runtime Checking of Service Substitutability (MMB, LC, AF, MP, MR), pp. 244–254.

EDOC-2010-Halle #contract #interface #ltl #monitoring #runtime

Cooperative Runtime Monitoring of LTL Interface Contracts (SH), pp. 227–236.

CAV-2010-CohenNS10a #composition #ltl #named #verification

SPLIT: A Compositional LTL Verifier (AC, KSN, YS), pp. 558–561.

ASE-2009-BarnatBS #clustering #ltl #model checking

Cluster-Based I/O-Efficient LTL Model Checking (JB, LB, PS), pp. 635–639.

TACAS-2009-PlakuKV #hybrid #ltl #safety

Falsification of LTL Safety Properties in Hybrid Systems (EP, LEK, MYV), pp. 368–382.

ICALP-v2-2009-KuhtzF #ltl

LTL Path Checking Is Efficiently Parallelizable (LK, BF), pp. 235–246.

IFM-2009-BenesBCSVZ #ltl #partial order #reduction

Partial Order Reduction for State/Event LTL (NB, LB, IC, JS, PV, BZ), pp. 307–321.

IFM-2009-VargasGTG #ltl #model checking

Model Checking LTL Formulae in RAISE with FDR (APV, AGG, SLTT, CG), pp. 231–245.

CAV-2009-FiliotJR #algorithm #ltl

An Antichain Algorithm for LTL Realizability (EF, NJ, JFR), pp. 263–277.

VMCAI-2009-GodefroidP #ltl #model checking #revisited

LTL Generalized Model Checking Revisited (PG, NP), pp. 89–104.

FoSSaCS-2008-Bojanczyk #ltl

The Common Fragment of ACTL and LTL (MB), pp. 172–185.

FoSSaCS-2008-DemriLS #automaton #ltl #model checking

Model Checking Freeze LTL over One-Counter Automata (SD, RL, AS), pp. 490–504.

TACAS-2008-BarnatBSW #ltl #model checking

Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking (JB, LB, PS, MW), pp. 48–62.

TACAS-2008-WulfDMR #algorithm #anti #ltl #model checking #named #satisfiability

Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking (MDW, LD, NM, JFR), pp. 63–77.

SEFM-2008-EdelkampS #ltl #model checking

Flash-Efficient LTL Model Checking with Minimal Counterexamples (SE, DS), pp. 73–82.

KR-2008-BaaderGL #axiom #logic #ltl

LTL over Description Logic Axioms (FB, SG, CL), pp. 684–694.

SEKE-2008-GarciaRS #automation #ltl #named #verification

PROTEF: Automatic Verification of Pattern-Based LTL Templates (LG, SR, SS), pp. 261–266.

CAV-2008-EdelkampSS #ltl #model checking

Semi-external LTL Model Checking (SE, PS, PS), pp. 530–542.

VMCAI-2008-MorgensternS #automaton #ltl

From LTL to Symbolically Represented Deterministic Automata (AM, KS), pp. 279–293.

VMCAI-2008-SohailSR #algorithm #game studies #hybrid #ltl

A Hybrid Algorithm for LTL Games (SS, FS, KR), pp. 309–323.

ICALP-2007-TorreP #complexity #model checking #on the #recursion #state machine

On the Complexity of LtlModel-Checking of Recursive State Machines (SLT, GP), pp. 937–948.

AMOST-2007-FraserW #generative #ltl #model checking #performance #testing #using

Using LTL rewriting to improve the performance of model-checker based test-case generation (GF, FW), pp. 64–74.

CADE-2007-PerezV #bound #effectiveness #encoding #logic #ltl #model checking

Encodings of Bounded LTL Model Checking in Effectively Propositional Logic (JANP, AV), pp. 346–361.

TACAS-2006-NiebertP #ltl #model checking #partial order #performance

Efficient Model Checking for LTL with Partial Order Snapshots (PN, DP), pp. 272–286.

FM-2006-GenonMM #algorithm #distributed #ltl #monitoring #performance #sequence

Monitoring Distributed Controllers: When an Efficient LTL Algorithm on Sequences Is Needed to Model-Check Traces (AG, TM, CM), pp. 557–572.

CAV-2006-RosuB #linear #logic #ltl #monitoring #synthesis

Allen Linear (Interval) Temporal Logic — Translation to LTL and Monitor Synthesis (GR, SB), pp. 263–277.

LICS-2006-DemriL #automaton #ltl #quantifier

LTL with the Freeze Quantifier and Register Automata (SD, RL), pp. 17–26.

LICS-2006-KahlonG #approach #ltl #model checking #thread

An Automata-Theoretic Approach for Model Checking Threads for LTL Propert (VK, AG), pp. 101–110.

TACAS-2005-HammerKM #ltl #model checking #on the fly

Truly On-the-Fly LTL Model Checking (MH, AK, SM), pp. 191–205.

TACAS-2005-HardingRS #algorithm #game studies #ltl #synthesis

A New Algorithm for Strategy Synthesis in LTL Games (AH, MR, PYS), pp. 477–492.

TACAS-2005-SchuppanB #ltl #model checking

Shortest Counterexamples for Symbolic Model Checking of LTL with Past (VS, AB), pp. 493–509.

DLT-J-2004-MuschollW05 #ltl

An NP-complete fragment of LTL (AM, IW), pp. 743–753.

CIAA-2005-PelanekS #automaton #ltl

Deeper Connections Between LTL and Alternating Automata (RP, JS), pp. 238–249.

CAV-2005-SebastianiTV #hybrid #ltl #model checking

Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking (RS, ST, MYV), pp. 350–363.

ICLP-2005-CorinSE #analysis #constraints #protocol #security

PS-LTL for Constraint-Based Security Protocol Analysis (RC, AS, SE), pp. 439–440.

VMCAI-2005-LatvalaBHJ #bound #ltl #model checking #performance

Simple Is Better: Efficient Bounded Model Checking for Past LTL (TL, AB, KH, TAJ), pp. 380–395.

FoSSaCS-2004-Demri #constraints #integer #ltl

LTL over Integer Periodicity Constraints: (Extended Abstract) (SD), pp. 121–135.

TACAS-2004-GeldenhuysV #algorithm #ltl #on the fly #performance #verification

Tarjan’s Algorithm Makes On-the-Fly LTL Verification More Efficient (JG, AV), pp. 205–219.

DLT-2004-MuschollW #ltl

An NP-Complete Fragment of LTL (AM, IW), pp. 334–344.

ICALP-2004-SamerV #ltl #query

A Syntactic Characterization of Distributive LTL Queries (MS, HV), pp. 1099–1110.

CAV-2004-AbdullaJNdS #ltl #model checking

Regular Model Checking for LTL(MSO) (PAA, BJ, MN, Jd, MS), pp. 348–360.

CAV-2004-SchroterK #model checking #parallel #petri net

Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings (CS, VK), pp. 109–121.

CSL-2004-Maier #liveness #ltl #safety

Intuitionistic LTL and a New Characterization of Safety and Liveness (PM), pp. 295–309.

ASE-2003-BarnatBC #ltl #model checking #parallel

Parallel Breadth-First Search LTL Model-Checking (JB, LB, JC), pp. 106–115.

TACAS-2003-BenedettiC #bound #ltl #model checking

Bounded Model Checking for Past LTL (MB, AC), pp. 18–33.

CSL-2003-KahlerW #complexity #ltl #model checking

Program Complexity of Dynamic LTL Model Checking (DK, TW), pp. 271–284.

ICLP-2003-Valencia03a #concurrent #constraints #decidability #ltl #programming

Timed Concurrent Constraint Programming: Decidability Results and Their Application to LTL (FDV), pp. 422–437.

WRLA-2002-EkerMS #ltl #maude #model checking

The Maude LTL Model Checker (SE, JM, AS), pp. 162–187.

SAS-2002-GallardoMP #ltl #model checking #refinement

Refinement of LTL Formulas for Abstract Model Checking (MdMG, PM, EP), pp. 395–410.

KR-2002-CalvaneseGV #ltl #reasoning

Reasoning about Actions and Planning in LTL Action Theories (DC, GDG, MYV), pp. 593–602.

CSL-2002-KuceraS #logic #ltl

The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL (AK, JS), pp. 276–291.

CSL-2002-MarcinkowskiT #bound #complexity #game studies #ltl

Optimal Complexity Bounds for Positive LTL Games (JM, TT), pp. 262–275.

VMCAI-2002-CimattiPRS #encoding #ltl #model checking #satisfiability

Improving the Encoding of LTL Model Checking into SAT (AC, MP, MR, RS), pp. 196–207.

FME-2001-LeuschelMC #csp #how #ltl #model checking #refinement

How to Make FDR Spin LTL Model Checking of CSP by Refinement (ML, TM, AC), pp. 99–118.

CAV-2001-GastinO #automaton #ltl #performance

Fast LTL to Büchi Automata Translation (PG, DO), pp. 53–65.

LICS-2001-AlurT #game studies #generative #ltl

Deterministic Generators and Games for LTL Fragments (RA, SLT), pp. 291–300.

ICALP-2000-DiekertG #ltl

LTL Is Expressively Complete for Mazurkiewicz Traces (VD, PG), pp. 211–222.

ICALP-2000-EsparzaH #approach #ltl #model checking

A New Unfolding Approach to LTL Model Checking (JE, KH), pp. 475–486.

CAV-2000-SomenziB #automaton #ltl #performance

Efficient Büchi Automata from LTL Formulae (FS, RB), pp. 248–263.

CAV-1998-Wallner #ltl #model checking #using

Model Checking LTL Using Net Unforldings (FW), pp. 207–218.

CAV-1994-ClarkeGH #ltl #model checking

Another Look at LTL Model Checking (EMC, OG, KH), pp. 415–427.