11

Take a path property that is not first-order expressible, e.g. $$\nu x.p\wedge\Diamond\Diamond x$$ which says that there exists a path where the atomic proposition $p$ holds at every even position, and any valuation can be used on odd positions.


6

The formula in your statement Obviously E(A(F1)) with F1=E(A(F1)) is not well-defined for some Büchi automata. So what does inductively defined exactly mean in this case? cannot arise if you built ECTL* inductively. This means, in standard academic parlance, we would present a syntax definition of the form below. Let $Prop$ be a set of propositions and $...


5

In general, CTL model checking is P-complete. Since we think that $L\neq P$ (and moreover $NL\neq P$), it is unlikely that an algorithm with logarithmic space exists. It is also unlikely that a sub-polynomial space algorithm exists, for similar reasons of common belief. I don't know of exact space-optimizations for the problem, but in general - yes, you ...


5

To expand on pedagand's answer: productivity is the term used for the computational dual (in some precise sense) of termination. Formally, a program f : CoData is productive if running the computation f eventually produces a constructor of CoData, and every (recursive) sub-term of that constructor is also productive. For example primes = filterBy prime [0.....


5

I think the key problem here is not understanding how inductive definitions of syntax work. Here are three approaches to understanding what a BNF grammar means. Consider a simple grammar: $$ t ::= \mathtt{true} ~~|~~ \mathtt{false} ~~|~~ 0 ~~|~~ \mathtt{succ}\ t ~~|~~ \mathtt{if}\ t\ \mathtt{then}\ t\ \mathtt{else}\ t$$ Following Pierce's Types and ...


4

I think the simpler example is your property, which can be written for instance $E(((a+b)a)^\omega))$. A simple way to show that is is not in CTL* is to show that this would imply that the word language $((a+b)a)^\omega$ is in LTL (because CTL* on linear structures is LTL). This fact is a classical result. To show it, it suffices (for instance) to use the ...


4

The answer to (1) is no, even for deterministic transducers. The reason is that we can encode configurations (tape contents + head position + machine state) of Turing machines into words such that the configuration changes made by any machine $M$ can be represented by a transducer $T_M$, and then decidability of (1) would imply decidability of the halting ...


4

Your first question is answered in this paper: https://www.cs.cornell.edu/fbs/publications/RecSafeLive.pdf Given an LTL formula, translate it into a Büchi automaton, and remove states that have no path to an accepting state. Then, change all states to be accepting. If the language of the automaton does not change, then the property is a safety property. ...


3

The "probabilistic" element in probabilistic model checking is that the system being checked is probabilistic, not that we add probabilities to an existing deterministic or non-deterministic system. Thus, what you are checking is whether a probabilistic system satisfies some property. For example "is it true that with probability at least 0.5, the system ...


3

Safety properties are closed under finite intersection. This can be seen by following Alpern and Schneider's characterisation which showed that safety properties are limit-closed when viewed topologically. Liveness properties as defined by Alpern and Schneider are dense. They are not closed under intersection as soon as there are two elements in the state ...


3

Q1: Yes, every LTS is bisimilar to its unfolding, which is a tree. Q2: No, by a cardinality argument. For instance take infinite binary trees with $L=\{a,b\}$. Each tree has countable set of states and is finitely-branching, but you have uncountably many such trees, even up to bisimilarity. However you have only countably many $\mu$-calculus formulas, so ...


3

For Q1, the answer is yes if we consider image-finite systems: for all node $t$ and label $a$, the number of $a$-successors of $t$ must be finite. In this case you don't even need fixpoints of the $\mu$-calculus, only the fragment called Hennessy-Milner Logic to distinguish non-bisimilar structures [HM85]. This is known as the Hennessy-Milner Theorem. ...


3

As time can be a resource, it is a bit unclear to me what you seek. Nevertheless, you might want to look at weighted extensions of LTL, like Metric Temporal Logic first defined here. (Specifying real-time properties with metric temporal logic)


3

In general, the technique used is known as "fuzzing". Not all errors are equally likely. Let's consider two hypothetical errors: System A incorrectly rejects a filename if it contains an | anywhere. System A incorrectly rejects a filename if it contains a prime number of b characters. Errors of the second type are much, much rarer, but this is not ...


3

You can find a formal model and proof of Paxos and Byzantine Paxos written by L. Lamport et al at http://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html. The model can be checked using the TLA+ toolbox. Notice that the author of the Paxos algorithm, the formal model above, and even the TLA+ modeling language is the same person:)


3

You could find a few examples in Danielsson's papers, such as: Total parser combinators Operational Semantics Using the Partiality Monad The key idea is to use the productivity of greatest fixpoints to guarantee liveness ("eventually something happens").


2

First question: A set $M$ is decidable if there is a Turing Machine which halts on all inputs and accepts all inputs $x$ with $x \in M$. We try to encode $\bigwedge_{\phi \in X} \phi$ for arbitrary sets of $\mathsf{FO}[\tau]$-formulars $X$. Since, $\mathcal{P}(X)$ is uncountable there can be no code with finite alphabet. Hence, there can be no Turing ...


2

For the concrete case of a specification of a regular language, there is the Java String Analyzer which roughly is able to compute a finite state automaton (i.e. regular expression) of the set of strings accepted by a Java method, using various techniques in static analysis. While the paper deals directly with the set of strings generated by a piece of Java ...


2

Your construction for bad prefixes is not correct on NBA's. For instance take the NBA on alphabet $A=\{a,b\}$ with two initial states $q_a$ and $q_b$ where for both $x\in A$, $q_x$ goes to an accepting sink if the first letter is $x$ and to a rejecting sink if the first letter is not $x$. Then the language recognized is $A^\omega$, but the set of "bad ...


2

Pierre Wolper defined in 1983 extended temporal logic (ETL, in Information and Computation 56, 72–99, doi:10.1016/S0019-9958(83)80051-5), where a temporal operator $\mathcal A(\varphi_1,\dots,\varphi_n)$ can be introduced for a finite-state automaton $\mathcal A$. The formula is satisfied in an infinite word $u$ at position $i$, i.e. $u,i\models\mathcal A(\...


2

To add to the answer in the comments, it might help to first ask what the difference is between a model checker and an automated theorem prover for propositional logic. Given the statement $$p \wedge q$$ we can ask whether it is true in the model $\{p=\top,q=\bot\}$ (model checking) or we can ask whether it is true in all models (theorem proving). We can ...


1

The answer is yes to all questions, so it is enough to answer 2 and 4, as the definitions work in particular for languages of finite words: A language $P\subseteq \Sigma^*\cup\Sigma^\omega$ is safety if whenever $u\notin P$, then $u$ has a finite prefix $u'\in\Sigma^*$ such that for any word $v$, $u'v\notin P$. A language $P\subseteq \Sigma^*\cup\Sigma^\...


1

I can think of 2 straight forward approaches Directly add $\forall xy (x < y \Rightarrow f(x) < f(y))$. Or Akcermannize the problem and add these as axioms for all pairs of terms.


1

What you wrote is correct. The actions $\textit{coin}$ and $\textit{ret_coin}$ do not change the values of the variables $\textit{Var} = \{\textit{nsoda}, \textit{nbeer}\}$, i.e., the number of soda and beer cans in the machine. Inserting a coin is only possible in the $\textit{start}$ location, and with this action the location changes to $\textit{select}$....


1

I'm assuming that you're really asking, "how do I do something useful with modelling and theory." The easiest answer is to work in a modelling and simulation field that makes useful products. Computational Electromagnetics is used a lot in RF, Finite Element Analysis is used in mechanical product design. The broken part of your reasoning is that "more ...


1

Maybe take a look at http://www.syntcomp.org/ This is a competition of tools solving the LTL synthesis problem (and some related problems).


1

I think it depends on what you mean by linear-time temporal logics. If you mean temporal logics that have linear time semantics (i.e. cannot distinguish more than trace equivalence, a la van Glabbeek) then there are indeed logics that require counter examples that are not just lassos. HyperLTL is an example: https://www.react.uni-saarland.de/publications/...


1

You may be aware of PRISM, a probabilistic model checker, and PRISM Case Studies which documents (besides others) case studies on the correctness and performance of various randomised distributed algorithms taken from the literature. It is quite common that one distributed computing problem has several variants (with different assumptions), and each variant ...


1

To answer your second question: there is one property that is both safety and liveness: True. With this exception, however, it is fair to say that a property is either safety or liveness or neither. "Most" properties (like yours) are actually neither, but every property can be represented by the intersection of a safety and a liveness property. I think ...


1

More along the "related formalisms" direction. PDL with intersection and converse: satisfiability and infinite-state model checking, Stefan Göller, Markus Lohrey, and Carsten Lutz, 2009 The Effects of Bounding Syntactic Resources on Presburger LTL, Stéphane Demri and Régis Gascon The introduction section of the first paper has an extensive discussion of ...


Only top voted, non community-wiki answers of a minimum length are eligible