# Tag Info

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

If the formula is satisfiable you cannot construct an interpolant. If the formula is unsatisfiable, you know that the final states are not reachable in at most $k$ steps. You do not know about reachability of final states in $k+1$ or more steps. If the formula you suggest is unsatisfiable, you can replace the sub-formula $I$ of $A$ with the interpolant and ...

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 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 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 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 ... 3 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 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 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 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 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"). 3 Intuitively, what happens here is that for$AFGp$, you check each individual path for whether after some point,$p$will always be true - no matter what other choices are available in a given state. In particular, for the path which always stays in the first state, this is true even though a$\neg p$-state is reachable. On all other paths it is true because ... 3 One thing we have to be clear on is the kind of property we are talking about: CTL and CTL* are branching-time logics, used to talk about tree languages, whereas LTL is a linear-time logic, which per se talks about words, but can be applied to trees by requiring all branches to satisfy the formula. This already gives you a hint for some CTL properties ... 3 I'm not answering the full question but only part of it (I have no interest in branching time). Your definition of$\mathit{even}$would better read$\mathit{even}(p) \equiv \exists q.(q \land \Box ( q \leftrightarrow \mathsf{X} \lnot q ) \land \Box ( q \rightarrow p ))$. You are introducing$q$only to remember if you are on an odd or even position, but ... 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 As it turns out, there is some fascinating work done in this direction. In particular, in 2003, Michael Howard, Jon Pincus, and Jeannette M. Wing's Measuring Relative Attack Surfaces in proceedings of Workshop on Advanced Developments in Software and Systems Security, Taipei, December 2003. Further work by the same authors over the years is quite ... 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 ... 2 I think that software model checking, in the vein of Alloy, is probably related to what you're looking for. You write a model, and also a specification that the model should satisfy, and check if they're related appropriately. 2 If your background is CTL interpreted over Kripke structures and you looks for something similar interpreted over LTSs, than ACTL (action-based CTL) could be interesting. Back in 1990, R. De Nicola and F. Vaandrager introduced ACTL as an action-based CTL (Action versus state based logics for transition systems, Semantics of Systems of Concurrent Processes (... 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(\...

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

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/...

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