2004/10/27 by Alexei Lisitsa, Lisitsa, Alexei, Igor Potapov +1 · 1 citation
Computer Science · #Computation and Language (cs.CL) #F.1.1 #F.3.1 #F.4.1 #F.4.3 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Multi-Agent Systems and Negotiation #cs.CL #cs.LO
paper · pdf · doi:10.48550/arxiv.cs/0410072
14 pages, 4 figures
arxiv created 2004/10/27 · openalex publication_date 2004/10/27 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
A predicate linear temporal logic LTLλ,= without quantifiers but with predicate abstraction mechanism and equality is considered. The models of LTLλ,= can be naturally seen as the systems of pebbles (flexible constants) moving over the elements of some (possibly infinite) domain. This allows to use LTLλ,= for the specification of dynamic systems using some resources, such as processes using memory locations, mobile agents occupying some sites, etc. On the other hand we show that LTLλ,= is not recursively axiomatizable and, therefore, fully automated verification of LTLλ,= specifications is not, in general, possible.