smtTranslation.bib

@article{tack20,
    author = {Menghi, Claudio and Bersani, Marcello M. and Rossi, Matteo and Pietro, Pierluigi San},
    title = {Model Checking MITL Formulae on Timed Automata: A Logic-Based Approach},
    year = {2020},
    issue_date = {May 2020},
    publisher = {Association for Computing Machinery},
    address = {New York, NY, USA},
    volume = {21},
    number = {3},
    issn = {1529-3785},
    url = {https://doi.org/10.1145/3383687},
    doi = {10.1145/3383687},
    abstract = {Timed Automata (TA) is de facto a standard modelling formalism to represent systems when the interest is the analysis of their behaviour as time progresses. This modelling formalism is mostly used for checking whether the behaviours of a system satisfy a set of properties of interest. Even if efficient model-checkers for Timed Automata exist, these tools are not easily configurable. First, they are not designed to easily allow adding new Timed Automata constructs, such as new synchronization mechanisms or communication procedures, but they assume a fixed set of Timed Automata constructs. Second, they usually do not support the Metric Interval Temporal Logic (MITL) and rely on a precise semantics for the logic in which the property of interest is specified, which cannot be easily modified and customized. Finally, they do not easily allow using different solvers that may speed up verification in different contexts.This article presents a novel technique to perform model checking of Metric Interval Temporal Logic (MITL) properties on TA. The technique relies on the translation of both the TA and the MITL formula into an intermediate Constraint LTL over clocks (CLTLoc) formula, which is verified through an available decision procedure. The technique is flexible, since the intermediate logic allows the encoding of new semantics as well as new TA constructs, by just adding new CLTLoc formulae. Furthermore, our technique is not bound to a specific solver as the intermediate CLTLoc formula can be verified using different procedures.},
    journal = {ACM Trans. Comput. Logic},
    month = apr,
    articleno = {26},
    numpages = {44},
    keywords = {timed automata, Model checking, signal-based semantics}
}

@inproceedings{baresi15,
author = {Baresi, Luciano and Pourhashem Kallehbasti, Mohammad Mehdi and Rossi, Matteo},
year = {2015},
month = {05},
pages = {},
title = {Efficient Scalable Verification of LTL Specifications},
doi = {10.1109/ICSE.2015.84}
}

@InProceedings{biere99,
author="Biere, Armin
and Cimatti, Alessandro
and Clarke, Edmund
and Zhu, Yunshan",
editor="Cleaveland, W. Rance",
title="Symbolic Model Checking without BDDs",
booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
year="1999",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="193--207",
abstract="Symbolic Model Checking [3], [14] has proven to be a powerful technique for the verification of reactive systems. BDDs [2] have traditionally been used as a symbolic representation of the system. In this paper we show how boolean decision procedures, like St{\aa}lmarck's Method [16] or the Davis {\&} Putnam Procedure [7], can replace BDDs. This new technique avoids the space blow up of BDDs, generates counterexamples much faster, and sometimes speeds up the verification. In addition, it produces counterexamples of minimal length. We introduce a bounded model checking procedure for LTL which reduces model checking to propositional satisfiability.We show that bounded LTL model checking can be done without a tableau construction. We have implemented a model checker BMC, based on bounded model checking, and preliminary results are presented.",
isbn="978-3-540-49059-3"
}

@InProceedings{kindermann12,
author="Kindermann, Roland
and Junttila, Tommi
and Niemel{\"a}, Ilkka",
editor="Giese, Holger
and Rosu, Grigore",
title="Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata",
booktitle="Formal Techniques for Distributed Systems",
year="2012",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="84--100",
abstract="Timed automata (TAs) are a common formalism for modeling timed systems. Bounded model checking (BMC) is a verification method that searches for runs violating a property using a SAT or SMT solver. Previous SMT-based BMC approaches for TAs search for finite counter-examples and infinite lasso-shaped counter-examples. This paper shows that lasso-based BMC cannot detect counter-examples for some linear time specifications expressed, e.g., with LTL or B{\"u}chi automata. This paper introduces a new SMT-based BMC approach that can find a counter-example to any non-holding B{\"u}chi automaton or LTL specification and also, in theory, prove that a specification holds. Different BMC encodings tailored for the supported features of different SMT solvers are compared experimentally to lasso-based BMC and discretization-based SAT BMC.",
isbn="978-3-642-30793-5"
}

@article{bersani15,
title = "An SMT-based approach to satisfiability checking of MITL",
journal = "Information and Computation",
volume = "245",
pages = "72 - 97",
year = "2015",
issn = "0890-5401",
doi = "https://doi.org/10.1016/j.ic.2015.06.007",
url = "http://www.sciencedirect.com/science/article/pii/S0890540115000747",
author = "Marcello M. Bersani and Matteo Rossi and Pierluigi {San Pietro}",
abstract = "We present a satisfiability-preserving reduction from MITL interpreted over finitely-variable continuous behaviors to Constraint LTL over clocks, a variant of CLTL that is decidable, and for which an SMT-based bounded satisfiability checker is available. The result is a new complete and effective decision procedure for MITL. Although decision procedures for MITL already exist, the automata-based techniques they employ appear to be very difficult to realize in practice, and, to the best of our knowledge, no implementation currently exists for them. A prototype tool for MITL based on the encoding presented here has, instead, been implemented and is publicly available."
}
@article{demri07,
title = "An automata-theoretic approach to constraint LTL",
journal = "Information and Computation",
volume = "205",
number = "3",
pages = "380 - 415",
year = "2007",
issn = "0890-5401",
doi = "https://doi.org/10.1016/j.ic.2006.09.006",
url = "http://www.sciencedirect.com/science/article/pii/S0890540106001076",
author = "Stéphane Demri and Deepak D’Souza",
keywords = "Temporal logic, Logics of space and time, Model-checking",
abstract = "We consider an extension of linear-time temporal logic (LTL) with constraints interpreted over a concrete domain. We use a new automata-theoretic technique to show PSPACE decidability of the logic for the constraint systems (Z,<,=) and (N,<,=). Along the way, we give an automata-theoretic proof of a result of Balbiani and Condotta when the constraint system satisfies the completion property. Our decision procedures extend easily to handle extensions of the logic with past-time operators and constants, as well as an extension of the temporal language itself to monadic second order logic. Finally we show that the logic becomes undecidable when one considers constraint systems that allow a counting mechanism."
}
@InProceedings{marconi16,
author="Marconi, Francesco
and Bersani, Marcello M.
and Erascu, Madalina
and Rossi, Matteo",
editor="Ogata, Kazuhiro
and Lawford, Mark
and Liu, Shaoying",
title="Towards the Formal Verification of Data-Intensive Applications Through Metric Temporal Logic",
booktitle="Formal Methods and Software Engineering",
year="2016",
publisher="Springer International Publishing",
address="Cham",
pages="193--209",
abstract="We present an approach for the automated formal verification of distributed systems based on the Storm technology. The approach is based on a formal model of the behavior of Storm topologies given in terms of the CLTLoc metric temporal logic extended with counters. We present a tool-supported mechanism to automatically generate formal models from high-level description of Storm topologies. The Zot formal verification tool is then used to check whether some desired properties hold for the modeled system or not. The analyzed properties concern the growth of the queues of the nodes of the Storm topology. Some experiments performed on example topologies show how the timing features of the modeled system influence the behavior of the queues of the nodes.",
isbn="978-3-319-47846-3"
}
@article{alur94,
title = "A theory of timed automata",
journal = "Theoretical Computer Science",
volume = "126",
number = "2",
pages = "183 - 235",
year = "1994",
issn = "0304-3975",
doi = "https://doi.org/10.1016/0304-3975(94)90010-8",
url = "http://www.sciencedirect.com/science/article/pii/0304397594900108",
author = "Rajeev Alur and David L. Dill",
abstract = "We propose timed (finite) automata to model the behavior of real-time systems over time. Our definition provides a simple, and yet powerful, way to annotate state-transition graphs with timing constraints using finitely many real-valued clocks. A timed automaton accepts timed words–infinite sequences in which a real-valued time of occurrence is associated with each symbol. We study timed automata from the perspective of formal language theory: we consider closure properties, decision problems, and subclasses. We consider both nondeterministic and deterministic transition structures, and both Büchi and Muller acceptance conditions. We show that nondeterministic timed automata are closed under union and intersection, but not under complementation, whereas deterministic timed Muller automata are closed under all Boolean operations. The main construction of the paper is an (PSPACE) algorithm for checking the emptiness of the language of a (nondeterministic) timed automaton. We also prove that the universality problem and the language inclusion problem are solvable only for the deterministic automata: both problems are undecidable (Π11-hard) in the nondeterministic case and PSPACE-complete in the deterministic case. Finally, we discuss the application of this theory to automatic verification of real-time requirements of finite-state systems."
}
@article{Alur91thebenefits,
author = {Alur, Rajeev and Feder, Tom\'{a}s and Henzinger, Thomas A.},
title = {The Benefits of Relaxing Punctuality},
year = {1996},
issue_date = {Jan. 1996},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {43},
number = {1},
issn = {0004-5411},
url = {https://doi.org/10.1145/227595.227602},
doi = {10.1145/227595.227602},
journal = {J. ACM},
month = jan,
pages = {116–146},
numpages = {31},
keywords = {real time, temporal logic, model checking, timed automata}
}




@article{bouyer09,
	doi = {10.1016/j.entcs.2009.02.044},
	url = {https://doi.org/10.1016%2Fj.entcs.2009.02.044},
	year = 2009,
	month = {mar},
	publisher = {Elsevier {BV}},
	volume = {231},
	pages = {323--341},
	author = {Patricia Bouyer},
	title = {Model-checking Timed Temporal Logics},
	journal = {Electronic Notes in Theoretical Computer Science}
}
@MISC{larsen97,
    author = {Kim G. Larsen and Paul Pettersson and Wang Yi},
    title = {UPPAAL in a Nutshell},
    year = {1997}
}
@article{kindermann13,
author = {Kindermann, Roland and Junttila, Tommi and Niemelä, Ilkka},
year = {2013},
month = {04},
pages = {},
title = {Bounded Model Checking of an MITL Fragment for Timed Automata},
journal = {Proceedings - International Conference on Application of Concurrency to System Design, ACSD},
doi = {10.1109/ACSD.2013.25}
}
@inproceedings{baresi16,
author = {Baresi, Luciano and Pourhashem Kallehbasti, Mohammad Mehdi and Rossi, Matteo},
title = {How Bit-Vector Logic Can Help Improve the Verification of LTL Specifications over Infinite Domains},
year = {2016},
isbn = {9781450337397},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2851613.2851833},
doi = {10.1145/2851613.2851833},
abstract = {Propositional Linear Temporal Logic (LTL) is well-suited for describing properties of timed systems in which data belong to finite domains. However, when one needs to capture infinite domains, as is typically the case in software systems, extensions of LTL are better suited to be used as specification languages. Constraint LTL (CLTL) and its variant CLTL-over-clocks (CLTLoc) are examples of such extensions; both logics are decidable, and so-called bounded decision procedures based on Satisfiability Modulo Theories (SMT) solving techniques have been implemented for them. In this paper we adapt a previously-introduced bounded decision procedure for LTL based on Bit-Vector Logic to deal with the infinite domains that are typical of CLTL and CLTLoc. We report on a thorough experimental comparison, which was carried out between the existing tool and the new, Bit-Vector Logic-based one, and we show how the latter outperforms the former in the vast majority of cases.},
booktitle = {Proceedings of the 31st Annual ACM Symposium on Applied Computing},
pages = {1666–1673},
numpages = {8},
keywords = {constraint LTL, logic integration, checking, formal verification, bounded satisfiability, bit-vector logic},
location = {Pisa, Italy},
series = {SAC '16}
}
@InProceedings{cimatti02,
author="Cimatti, Alessandro
and Clarke, Edmund
and Giunchiglia, Enrico
and Giunchiglia, Fausto
and Pistore, Marco
and Roveri, Marco
and Sebastiani, Roberto
and Tacchella, Armando",
editor="Brinksma, Ed
and Larsen, Kim Guldstrand",
title="NuSMV 2: An OpenSource Tool for Symbolic Model Checking",
booktitle="Computer Aided Verification",
year="2002",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="359--364",
abstract="This paper describes version 2 of the NuSMV tool. NuSMV is a symbolic model checker originated from the reengineering, reimplementation and extension of SMV, the original BDD-based model checker developed at CMU [15]. The NuSMV project aims at the development of a state-of-the-art symbolic model checker, designed to be applicable in technology transfer projects: it is a well structured, open, flexible and documented platform for model checking, and is robust and close to industrial systems standards [6].",
isbn="978-3-540-45657-5"
}
@article{burch92,
title = "Symbolic model checking: 1020 States and beyond",
journal = "Information and Computation",
volume = "98",
number = "2",
pages = "142 - 170",
year = "1992",
issn = "0890-5401",
doi = "https://doi.org/10.1016/0890-5401(92)90017-A",
url = "http://www.sciencedirect.com/science/article/pii/089054019290017A",
author = "J.R. Burch and E.M. Clarke and K.L. McMillan and D.L. Dill and L.J. Hwang",
abstract = "Many different methods have been devised for automatically verifying finite state systems by examining state-graph models of system behavior. These methods all depend on decision procedures that explicitly represent the state space using a list or a table that grows in proportion to the number of states. We describe a general method that represents the state space symbolically instead of explicitly. The generality of our method comes from using a dialect of the Mu-Calculus as the primary specification language. We describe a model checking algorithm for Mu-Calculus formulas that uses Bryant's Binary Decision Diagrans (Bryant, R. E., 1986, IEEE Trans. Comput.C-35) to represent relations and formulas. We then show how our new Mu-Calculus model checking algorithm can be used to derive efficient decision procedures for CTL model checking, satisfiability of linear-time temporal logic formulas, strong and weak observational equivalence of finite transition systems, and language containment for finite ω-automata. The fixed point computations for each decision procedure are sometimes complex, but can be concisely expressed in the Mu-Calculus. We illustrate the practicality of our approach to symbolic model checking by discussing how it can be used to verify a simple synchronous pipeline circuit."
}
@article{bryant86,
author = {Bryant, Randal},
year = {1986},
month = {09},
pages = {677 - 691},
title = {Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Computers 35(8), 677-691},
volume = {C-35},
journal = {Computers, IEEE Transactions on},
doi = {10.1109/TC.1986.1676819}
}

@MISC{BarFT-SMTLIB,
  author =	 {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
  title =	 {{The Satisfiability Modulo Theories Library (SMT-LIB)}},
  howpublished = {{\tt www.SMT-LIB.org}},
  year =	 2016,
}