Hi Thomas, thanks very much for these background info and paper links (I only know&read one of them before). Honestly speaking, I didn’t notice the existence of “example/temporal_deep” folder before.
I’m currently working in the Italy research group who developed NuSMV and nuXmv model checkers. They internally used the same symbolic algorithm as the work in HOL’s "src/temporal”. And I’m trying to make sure all my future LTL-based work are formally verified, and with HOL4 I actually have such many different choices, that’s great. Any way, I’ll read all the relevant materials before making a decision on which one to base upon. Regards, Chun Tian > Il giorno 21 mag 2018, alle ore 19:30, Thomas Tuerk <tho...@tuerk-brechen.de> > ha scritto: > > Hi, > > I worked with the other formalisation in "src/temporal" by Klaus Schneider > briefly for my master thesis in 2004/2005 supervised by Prof. Schneider. As > far as I remember (ages ago), one of the main points is a translation of LTL > into symbolically represented omega-automata. There is a paper by Prof. > Schneider about it, which mentions this translation: > > K. Schneider. Improving automata generation for linear temporal logic by > considering the automata hierarchy. > In Logic for Programming, Articial Intelligence, and Reasoning (LPAR), volume > 2250 of LNAI, Havanna, Cuba, 2001. Springer. > https://es.cs.uni-kl.de/publications/datarsg/Schn01b.pdf > It is -- as you said -- a shallow embedding and I believe it focuses on > automata formulae and this translation of LTL into automata formulae. For my > master thesis I created a deep embedding of this algorithm. I translated a > subset of PSL into LTL and then used this algorithm to get omega automata. I > used a deep embedding partly because I had no clue what I was doing (it was > the very first time I used HOL 4) and partly because I cared about things > like counting the number of occurrences of certain operators in the LTL > formulae. This work can be found in "examples/temporal_deep". > > There used to be a debate whether alternating omega automata or symbolically > represented nondeterministic / universal ones are better for certain model > checking problems (efficiency of certain implementations, algorithms, ...). > As part of an investigation into this, I extended the work in > "examples/temporal_deep" with a deep embedding of alternating automate and > verified a few algorithms. It's ages ago, but I believe that while for > specific instances it might be better to use automata formulae, in general > the alternating ones that seem to be implemented in "examples/logic/ltl" are > superior for most applications. A technical report of my thoughts at that > time is available at > > The stuff in "examples/temporal_deep" got also extended for model checking > PSL using HOL and SMV. > > http://www.thomas-tuerk.de/publications/Tuer05.pdf (my master thesis, lengthy > and poor English (the very first technical document I wrote in English)) > http://www.thomas-tuerk.de/publications/TuSc05.pdf (my master thesis as > published at ITP 2005) > http://www.thomas-tuerk.de/publications/TuSc05a.pdf (comparing alternating > automata and symbolically represented ones) > http://www.thomas-tuerk.de/publications/TuSG07.pdf (PSL model checking) > > Cheers > > Thomas > > > On 21.05.2018 14:40, Chun Tian wrote: >> Hi Michael, >> >> thanks for the explanation and paper link! >> >> Regards, >> >> Chun >> >> >>> Il giorno 20 mag 2018, alle ore 11:56, michael.norr...@data61.csiro.au >>> ha scritto: >>> >>> The paper describing the work in examples/logic/ltl will appear at ITP this >>> year. Because there's a slight CakeML angle to it, it's available from >>> cakeml.org at >>> https://cakeml.org/itp18.pdf >>> . >>> >>> You are right that this work could be described as a deep embedding. >>> >>> Deep embeddings usually have the advantage that you can describe algorithms >>> on the syntax, and not just have to think about the semantic values. For >>> example, you can describe the NNF transformation when you have a deep >>> embedding, but the best option for something similar with a shallow >>> embedding is a statement of some equivalences between different semantic >>> formulations of the same thing. >>> >>> It's also obviously useful to have a type corresponding to the syntax if >>> you are going to define computable functions to traverse over it and >>> transform it into automata (as is done in our work). >>> >>> Michael >>> >>> On 19/5/18, 00:42, "Chun Tian" >>> <binghe.l...@gmail.com> >>> wrote: >>> >>> Hi, >>> >>> I saw how the new LTL formalization (in `examples/logic/ltl`) by Simon >>> Jantsch suddenly appeared in the past months and because more and more >>> complete also with help of HOL maintainers. But there’s already an older >>> LTL formalization (in `src/temporal`) since long time ago, done by Klaus >>> Schneider et al. [1] >>> >>> My first question: is there a paper (in PDF, published or unpublished) >>> documenting the work in `examples/logic/ltl` so that I can learn beside >>> looking at raw HOL scripts? >>> >>> Second question: regarding the difference between two versions of LTL >>> formalizations, can I say the work in `examples/logic/ltl` is a *deep* >>> embedding? (because it has to define the LTL syntax by a datatype: >>> >>> val _ = Datatype` >>> ltl_frml >>> = VAR 'a >>> | N_VAR 'a >>> | DISJ ltl_frml ltl_frml >>> | CONJ ltl_frml ltl_frml >>> | X ltl_frml >>> | U ltl_frml ltl_frml >>> | R ltl_frml ltl_frml`; >>> ) >>> >>> while the work in `src/temporal` is *shallow* embedding? (because it >>> embeds LTL term into HOL as ``:num -> bool`` without using any datatype) >>> >>> and if so, what’s the pros and cons for choosing one of them as a >>> working basis (for proving further results)? >>> >>> Third question: is there a way to connect the two versions of LTL, so >>> that LTL theorems proved from one side can be (somehow) automatically >>> translated into theorems on the other side? >>> >>> Regards, >>> >>> Chun >>> >>> [1] Schneider, K., Hoffmann, D.W.: A HOL Conversion for Translating >>> Linear Time Temporal Logic to ω-Automata. In: Bassiliades, N., Gottlob, G., >>> Sadri, F., Paschke, A., and Roman, D. (eds.) LNCS 9202 - Rule Technologies: >>> Foundations, Tools, and Applications. pp. 255–272. Springer Berlin >>> Heidelberg, Berlin, Heidelberg (1999). >>> >>> >>> >>> >>> >>> >>> >>> ------------------------------------------------------------------------------ >>> Check out the vibrant tech community on one of the world's most >>> engaging tech sites, Slashdot.org! >>> http://sdm.link/slashdot >>> >>> _______________________________________________ >>> hol-info mailing list >>> >>> hol-info@lists.sourceforge.net >>> https://lists.sourceforge.net/lists/listinfo/hol-info >> >> >> ------------------------------------------------------------------------------ >> Check out the vibrant tech community on one of the world's most >> engaging tech sites, Slashdot.org! >> http://sdm.link/slashdot >> >> >> _______________________________________________ >> hol-info mailing list >> >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info > > ------------------------------------------------------------------------------ > Check out the vibrant tech community on one of the world's most > engaging tech sites, Slashdot.org! > http://sdm.link/slashdot_______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info
signature.asc
Description: Message signed with OpenPGP
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
