diff --git a/doc/spot.bib b/doc/spot.bib index 027ec695a..87259d815 100644 --- a/doc/spot.bib +++ b/doc/spot.bib @@ -12,7 +12,8 @@ publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {7214}, - pages = {95--109} + pages = {95--109}, + doi = {10.1007/978-3-642-28756-5_8} } @InProceedings{ babiak.13.spin, @@ -45,7 +46,8 @@ series = {Lecture Notes in Computer Science}, pages = {445--461}, month = oct, - publisher = {Springer} + publisher = {Springer}, + doi = {10.1007/978-3-030-31784-3_26} } @InProceedings{ beer.01.cav, @@ -61,7 +63,8 @@ pages = {363--367}, volume = {2102}, year = {2001}, - month = jul + month = jul, + doi = {10.1007/3-540-44585-4_33} } @InProceedings{ benedikt.13.tacas, @@ -75,7 +78,8 @@ series = {Lecture Notes in Computer Science}, volume = {7795}, editor = {Nir Piterman and Scott A. Smolka}, - publisher = {Springer} + publisher = {Springer}, + doi = {10.1007/978-3-642-36742-7_3} } @Article{ boker.2011.fossacs, @@ -85,7 +89,8 @@ Structures - 14th International Conference, FOSSACS 2011}, year = {2011}, pages = {184--198}, - url = {http://www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf} + url = {http://www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}, + doi = {10.1007/978-3-642-19805-2_13} } @Article{ bruggeman.96.tcs, @@ -94,7 +99,8 @@ journal = {Theoretical Computer Science}, year = {1996}, volume = {120}, - pages = {87--98} + pages = {87--98}, + doi = {10.1007/BFb0023820} } @Article{ carton.99.ita, @@ -104,7 +110,8 @@ year = {1999}, volume = {33}, number = {6}, - pages = {495--505} + pages = {495--505}, + url = {http://www.numdam.org/item/ITA_1999__33_6_495_0/} } @InProceedings{ cerna.03.mfcs, @@ -120,7 +127,8 @@ series = {Lecture Notes in Computer Science}, address = {Bratislava, Slovak Republic}, month = aug, - publisher = {Springer-Verlag} + publisher = {Springer-Verlag}, + doi = {10.1007/978-3-540-45138-9_26} } @InProceedings{ chang.92.icalp, @@ -131,7 +139,8 @@ year = {1992}, pages = {474--486}, publisher = {Springer-Verlag}, - address = {London, UK} + address = {London, UK}, + doi = {10.1007/3-540-55719-9_97} } @InProceedings{ cichon.09.depcos, @@ -142,7 +151,8 @@ Dependability of Computer Systems}, pages = {17--24}, year = 2009, - publisher = {IEEE Computer Society} + publisher = {IEEE Computer Society}, + doi = {10.1109/DepCoS-RELCOMEX.2009.31} } @Article{ cimatti.08.tcad, @@ -155,7 +165,8 @@ volume = 27, year = 2008, date = {2009-03-20}, - url = {https://es.fbk.eu/people/tonetta/tests/tcad07/} + url = {https://es.fbk.eu/people/tonetta/tests/tcad07/}, + doi = {10.1109/TCAD.2008.2003303} } @Article{ courcoubetis.92.fmsd, @@ -166,7 +177,8 @@ journal = {Formal Methods in System Design}, pages = {275--288}, year = {1992}, - volume = {1} + volume = {1}, + doi = {10.1007/BF00121128} } @InProceedings{ couvreur.99.fm, @@ -181,7 +193,8 @@ volume = {1708}, year = {1999}, month = sep, - isbn = {3-540-66587-0} + isbn = {3-540-66587-0}, + doi = {10.1007/3-540-48119-2_16} } @InProceedings{ dax.07.atva, @@ -197,7 +210,8 @@ (ATVA'07)}, editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino and Yoshio Okamura}, - month = oct + month = oct, + doi = {10.1007/978-3-540-75596-8_17} } @InProceedings{ dax.09.atva, @@ -211,7 +225,8 @@ year = {2009}, volume = {5799}, series = {Lecture Notes in Computer Science}, - publisher = {Springer-Verlag} + publisher = {Springer-Verlag}, + doi = {10.1007/978-3-642-04761-9_19} } @InProceedings{ duret.11.vecos, @@ -257,7 +272,8 @@ editor = {Mark Ardis}, month = mar, year = 1998, - pages = {7--15} + pages = {7--15}, + doi = {10.1145/298595.298598} } @Book{ eisner.06.psl, @@ -265,7 +281,8 @@ title = {A Practical Introduction to {PSL}}, publisher = {Springer}, year = {2006}, - series = {Series on Integrated Circuits and Systems} + series = {Series on Integrated Circuits and Systems}, + doi = {10.1007/978-0-387-36123-9} } @InCollection{ eisner.08.hvc, @@ -280,7 +297,8 @@ pages = {164--178}, volume = {5394}, year = {2009}, - month = oct + month = oct, + doi = {10.1007/978-3-642-01702-5_17} } @InProceedings{ etessami.00.concur, @@ -301,7 +319,8 @@ \url{http://www.bell-labs.com/project/TMP/} is fixed. We fixed the bug in Spot in 2005, thanks to LBTT. See also \url{http://arxiv.org/abs/1011.4214v2} for a discussion - about this problem.} + about this problem.}, + doi = {10.1007/3-540-44618-4_13} } @Article{ etessami.00.ipl, @@ -312,7 +331,8 @@ volume = {75}, number = {6}, year = {2000}, - pages = {261--263} + pages = {261--263}, + doi = {10.1016/S0020-0190(00)00113-7} } @InProceedings{ gastin.01.cav, @@ -325,7 +345,8 @@ editor = {G. Berry and H. Comon and A. Finkel}, volume = {2102}, series = {Lecture Notes in Computer Science}, - publisher = {Springer-Verlag} + publisher = {Springer-Verlag}, + doi = {10.1007/3-540-44585-4_6} } @InProceedings{ geldenhuys.04.tacas, @@ -341,7 +362,8 @@ publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2988}, - isbn = {3-540-21299-X} + isbn = {3-540-21299-X}, + doi = {10.1007/978-3-540-24730-2_18} } @InProceedings{ geldenhuys.06.spin, @@ -353,7 +375,8 @@ pages = {53--70}, series = {Lecture Notes in Computer Science}, volume = {3925}, - publisher = {Springer} + publisher = {Springer}, + doi = {10.1007/11691617_4} } @TechReport{ holevek.04.tr, @@ -363,7 +386,8 @@ month = {September}, year = 2004, number = 03, - institution = {CESNET} + institution = {CESNET}, + url = {http://archiv.cesnet.cz/doc/techzpravy/2004/verificationresults/} } @Book{ holzmann.91.book, @@ -371,7 +395,8 @@ title = {Design and Validation of Computer Protocols}, publisher = {Prentice-Hall}, address = {Englewood Cliffs, New Jersey}, - year = {1991} + year = {1991}, + isbn = {978-0-13-539925-5} } @InProceedings{ jacobs.16.synt, @@ -408,7 +433,6 @@ year = 2012, pages = {7--22}, doi = {10.1007/978-3-642-31424-7_7}, - url = {https://doi.org/10.1007/978-3-642-31424-7_7}, isbn = {978-3-642-31424-7}, publisher = {Springer} } @@ -435,7 +459,8 @@ pages = {408--429}, volume = {2}, number = {3}, - publisher = {ACM New York, NY, USA} + publisher = {ACM New York, NY, USA}, + doi = {10.1145/377978.377993} } @Article{ kupferman.05.tcl, @@ -461,7 +486,8 @@ pages = {83--100}, volume = {345}, number = {1}, - publisher = {Elsevier} + publisher = {Elsevier}, + doi = {10.1007/978-3-540-24730-2_43} } @InProceedings{ kupferman.10.mochart, @@ -486,7 +512,8 @@ and Connection to Second Order Logic}, school = {Institute of Computer Science and Applied Mathematics Christian-Albrechts-University of Kiel}, - year = {1998} + year = {1998}, + url = {https://old.automata.rwth-aachen.de/users/loeding/diploma_loeding.pdf} } @InProceedings{ loding.99.fstts, @@ -512,7 +539,8 @@ volume = {27}, number = {3}, pages = {163--182}, - month = aug + month = aug, + doi = {10.1016/0020-0255(82)90023-8} } @InProceedings{ manna.87.podc, @@ -524,7 +552,8 @@ location = {Quebec City, Canada}, pages = {377--410}, publisher = {ACM}, - address = {New York, NY, USA} + address = {New York, NY, USA}, + doi = {10.1145/93385.93442} } @InProceedings{ michaud.15.spin, @@ -538,7 +567,8 @@ series = {Lecture Notes in Computer Science}, volume = 9232, publisher = {Springer}, - month = aug + month = aug, + doi = {10.1007/978-3-319-23404-5_7} } @InProceedings{ minato.92.sasimi, @@ -550,7 +580,7 @@ pages = {64--73}, year = {1992}, address = {Kobe, Japan}, - month = {April} + month = apr } @InProceedings{ muller.17.gandalf, @@ -576,7 +606,8 @@ numpages = {5}, volume = {4595}, series = {Lecture Notes in Computer Science}, - publisher = {Springer-Verlag} + publisher = {Springer-Verlag}, + doi = {10.1007/978-3-540-73370-6_17} } @InProceedings{ piterman.06.vmcai, @@ -590,7 +621,8 @@ publisher = {Springer}, pages = {364--380}, volume = {3855}, - series = {Lecture Notes in Computer Science} + series = {Lecture Notes in Computer Science}, + doi = {10.1007/11609773_24} } @Book{ psl.04.lrm, @@ -609,7 +641,8 @@ year = {2012}, volume = {119}, number = {3-4}, - pages = {393--496} + pages = {393--406}, + doi = {10.3233/FI-2012-744} } @InProceedings{ renault.13.tacas, @@ -637,7 +670,8 @@ year = 2007, volume = {4595}, series = {Lecture Notes in Computer Science}, - publisher = {Springer-Verlag} + publisher = {Springer-Verlag}, + doi = {10.1007/978-3-540-73370-6_11} } @InProceedings{ schneider.01.lpar, @@ -651,7 +685,8 @@ volume = {2250}, series = {Lecture Notes in Artificial Intelligence}, address = {Havana, Cuba}, - publisher = {Springer-Verlag} + publisher = {Springer-Verlag}, + doi = {10.1007/3-540-45653-8_3} } @TechReport{ schwoon.04.tr, @@ -678,7 +713,8 @@ volume = {2860}, series = {Lectures Notes in Computer Science}, month = {October}, - publisher = {Springer-Verlag} + publisher = {Springer-Verlag}, + doi = {10.1007/978-3-540-39724-3_12} } @InProceedings{ sickert.16.cav, @@ -698,7 +734,7 @@ @InProceedings{ somenzi.00.cav, author = {Fabio Somenzi and Roderick Bloem}, - title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}}, + title = {Efficient {B\"u}chi Automata for {LTL} Formulae}, booktitle = {Proceedings of the 12th International Conference on Computer Aided Verification (CAV'00)}, pages = {247--263}, @@ -706,7 +742,8 @@ volume = {1855}, series = {Lecture Notes in Computer Science}, address = {Chicago, Illinois, USA}, - publisher = {Springer-Verlag} + publisher = {Springer-Verlag}, + doi = {10.1007/10722167_21} } @Book{ systemverilog.18.std, @@ -728,7 +765,8 @@ volume = {6418}, series = {Lecture Notes in Computer Science}, month = nov, - publisher = {Springer} + publisher = {Springer}, + doi = {10.1007/978-3-642-16612-9_33} } @TechReport{ tauriainen.00.tr, @@ -741,7 +779,8 @@ number = {A66}, year = {2000}, type = {Research Report}, - note = {Reprint of Master's thesis} + note = {Reprint of Master's thesis}, + url = {http://www.tcs.hut.fi/Publications/A66.shtml} } @TechReport{ tauriainen.03.tr, @@ -756,7 +795,8 @@ Nondeterministic Automata}, type = {Research Report}, year = {2003}, - note = {Reprint of Licentiate's thesis} + note = {Reprint of Licentiate's thesis}, + url = {http://www.tcs.hut.fi/Publications/A83.shtml} } @TechReport{ tauriainen.06.tr, @@ -768,7 +808,8 @@ title = {Automata and Linear Temporal Logic: Translations with Transition-Based Acceptance}, type = {Research Report}, - year = {2006} + year = {2006}, + url = {http://www.tcs.hut.fi/Publications/A104.shtml} } @InProceedings{ thirioux.02.fmics, @@ -783,7 +824,8 @@ editor = {Rance Cleaveland and Hubert Garavel}, year = {2002}, month = jul, - address = {M{\'a}laga, Spain} + address = {M{\'a}laga, Spain}, + doi = {10.1016/S1571-0661(04)80409-2} } @InBook{ thomas.97.chapter, @@ -793,7 +835,8 @@ editor = {Grzegorz Rozenberg and Arto Salomaa}, chapter = 7, publisher = {Springer-Verlag}, - year = {1997} + year = {1997}, + doi = {10.1007/978-3-642-59126-6_7} } @Article{ zielonka.98.tcs, @@ -804,5 +847,6 @@ volume = {200}, number = {1}, pages = {135--183}, - year = {1998} + year = {1998}, + doi = {10.1016/S0304-3975(98)00009-7} } diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 2406f0084..066bf1c94 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -16,6 +16,7 @@ %\usepackage{showlabels} \usepackage{tabulary} \usepackage[numbers]{natbib} +\usepackage{doi} \usepackage{rotating} \usepackage{booktabs} \usepackage{tikz} @@ -789,7 +790,7 @@ it for output. $b$ must be a Boolean formula. \end{align*} The following adds input support for the SVA concatenation (or delay) -operator~\cite{systemverilog.04.lrm}. The simplest equivalence are +operator~\cite{systemverilog.18.std}. The simplest equivalence are that $f \DELAY{0} g$, $f \DELAY{1} g$, $f \DELAY{2} g$ mean respectively $f \FUSION g$, $f \CONCAT g$, and $f \CONCAT \1\CONCAT g$, but the delay can be a range, and $f$ can be