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
