I dont understand the G syntax in a LTL (linear temporal logic) formula
$begingroup$
I know it states: "G for always (globally)"
But what does this mean? Is this the "same" as A for CTL syntax?
What is the difference between
M |= AG EF p (this i read as globally for all paths there exists a path where evenutally p is true)
and
M |= A EF p
It seems that G in LTL is very similar to A in CTL
logic
asked Jan 6 at 13:53
Felix RosénFelix Rosén
1304
$endgroup$
add a comment |
$begingroup$
I know it states: "G for always (globally)"
But what does this mean? Is this the "same" as A for CTL syntax?
What is the difference between
M |= AG EF p (this i read as globally for all paths there exists a path where evenutally p is true)
and
M |= A EF p
It seems that G in LTL is very similar to A in CTL
logic
asked Jan 6 at 13:53
Felix RosénFelix Rosén
1304
$endgroup$
1
$begingroup$
See LTL.
$endgroup$
– Mauro ALLEGRANZA
Jan 6 at 13:58
$begingroup$
@MauroALLEGRANZA Where do you think I got literally my first scentence from? What does it mean to "Globally: φ has to hold on the entire subsequent path." That all states have L(state) = φ?
$endgroup$
– Felix Rosén
Jan 6 at 14:01
add a comment |
$begingroup$
I know it states: "G for always (globally)"
But what does this mean? Is this the "same" as A for CTL syntax?
What is the difference between
M |= AG EF p (this i read as globally for all paths there exists a path where evenutally p is true)
and
M |= A EF p
It seems that G in LTL is very similar to A in CTL
logic
asked Jan 6 at 13:53
Felix RosénFelix Rosén
1304
$endgroup$
I know it states: "G for always (globally)"
But what does this mean? Is this the "same" as A for CTL syntax?
What is the difference between
M |= AG EF p (this i read as globally for all paths there exists a path where evenutally p is true)
and
M |= A EF p
It seems that G in LTL is very similar to A in CTL
logic
logic
asked Jan 6 at 13:53
Felix RosénFelix Rosén
1304
asked Jan 6 at 13:53
Felix RosénFelix Rosén
1304
asked Jan 6 at 13:53
Felix RosénFelix Rosén
1304
asked Jan 6 at 13:53
Felix RosénFelix Rosén
1304
asked Jan 6 at 13:53
Felix RosénFelix Rosén
1304
1304
1
$begingroup$
See LTL.
$endgroup$
– Mauro ALLEGRANZA
Jan 6 at 13:58
$begingroup$
@MauroALLEGRANZA Where do you think I got literally my first scentence from? What does it mean to "Globally: φ has to hold on the entire subsequent path." That all states have L(state) = φ?
$endgroup$
– Felix Rosén
Jan 6 at 14:01
add a comment |
1
$begingroup$
See LTL.
$endgroup$
– Mauro ALLEGRANZA
Jan 6 at 13:58
$begingroup$
@MauroALLEGRANZA Where do you think I got literally my first scentence from? What does it mean to "Globally: φ has to hold on the entire subsequent path." That all states have L(state) = φ?
$endgroup$
– Felix Rosén
Jan 6 at 14:01
1
1
$begingroup$
See LTL.
$endgroup$
– Mauro ALLEGRANZA
Jan 6 at 13:58
$begingroup$
See LTL.
$endgroup$
– Mauro ALLEGRANZA
Jan 6 at 13:58
$begingroup$
@MauroALLEGRANZA Where do you think I got literally my first scentence from? What does it mean to "Globally: φ has to hold on the entire subsequent path." That all states have L(state) = φ?
$endgroup$
– Felix Rosén
Jan 6 at 14:01
$begingroup$
@MauroALLEGRANZA Where do you think I got literally my first scentence from? What does it mean to "Globally: φ has to hold on the entire subsequent path." That all states have L(state) = φ?
$endgroup$
– Felix Rosén
Jan 6 at 14:01
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
$mathsf{G}$ is a temporal operator (or modality). $pi models mathsf{G} p$ means that $p$ holds at all states of path $pi$.
$mathsf{A}$ is a path quantifier. In CTL and CTL$^*$, $mathsf A$ quantifies over all the paths originating from a state. In LTL it is as if there were an implicit $mathsf A$ in front of the whole formula. In fact, to translate from LTL to CTL$^*$, one simply adds an $mathsf{A}$ in front of the LTL formula.
The first example you gave, $M models mathsf{AG,EF} ,p$, concerns a CTL formula that says that from all states of $M$ reachable from the initial states of $M$ there originates a path along which $p$ eventually holds. (This property is often called resetability, because $p$ may be chosen to distinguish the reset states of the model.)
The second example you gave, $M models mathsf{A,EF} ,p$, concerns a CTL$^*$ formula equivalent to $mathsf{EF} ,p$. $M$ satisfies $mathsf{EF} ,p$ if, from all initial states of $M$, a state where $p$ holds is reachable.
Neither example is expressible in LTL. Both require branching time.
Perhaps, the CTL (and CTL$^*$) formula $mathsf{AG} ,p$ illustrates the difference between $mathsf{A}$ and $mathsf{G}$ best. In English, $M,s modelsmathsf{AG} ,p$ says "along all states of all paths of $M$ originating from state $s$, $p$ holds." Both $mathsf{A}$ and $mathsf{G}$ are necessary in CTL to express that $p$ is invariant in $M$.
In LTL one simply skips the initial (implicit) $mathsf A$, because the definition of $M models varphi$, when $M$ is a Kripke structure, incorporates the universal quantification over the paths originating from the initial states of $M$.
Consider a Kripke structure $M$ with states ${0,1,2}$, initial states ${0}$, and the following transition relation,
$$ {(0,1),(0,2),(1,2),(2,2)} enspace. $$
Suppose that the atomic proposition $p$ holds at states $0$ and $2$. Then we have $M models mathsf{F} p$, but $M notmodels mathsf{G} p$. If $pi_1$ is the path $0,1,2,2,ldots$ and $pi_2$ is the path $0,2,2,ldots$, then $pi_2 models mathsf{G} p$, but $pi_1 notmodels mathsf{G} p$; hence $M notmodels mathsf{G} p$.
answered Jan 6 at 14:40
Fabio SomenziFabio Somenzi
6,41321221
$endgroup$
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3063882%2fi-dont-understand-the-g-syntax-in-a-ltl-linear-temporal-logic-formula%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
$mathsf{G}$ is a temporal operator (or modality). $pi models mathsf{G} p$ means that $p$ holds at all states of path $pi$.
$mathsf{A}$ is a path quantifier. In CTL and CTL$^*$, $mathsf A$ quantifies over all the paths originating from a state. In LTL it is as if there were an implicit $mathsf A$ in front of the whole formula. In fact, to translate from LTL to CTL$^*$, one simply adds an $mathsf{A}$ in front of the LTL formula.
The first example you gave, $M models mathsf{AG,EF} ,p$, concerns a CTL formula that says that from all states of $M$ reachable from the initial states of $M$ there originates a path along which $p$ eventually holds. (This property is often called resetability, because $p$ may be chosen to distinguish the reset states of the model.)
The second example you gave, $M models mathsf{A,EF} ,p$, concerns a CTL$^*$ formula equivalent to $mathsf{EF} ,p$. $M$ satisfies $mathsf{EF} ,p$ if, from all initial states of $M$, a state where $p$ holds is reachable.
Neither example is expressible in LTL. Both require branching time.
Perhaps, the CTL (and CTL$^*$) formula $mathsf{AG} ,p$ illustrates the difference between $mathsf{A}$ and $mathsf{G}$ best. In English, $M,s modelsmathsf{AG} ,p$ says "along all states of all paths of $M$ originating from state $s$, $p$ holds." Both $mathsf{A}$ and $mathsf{G}$ are necessary in CTL to express that $p$ is invariant in $M$.
In LTL one simply skips the initial (implicit) $mathsf A$, because the definition of $M models varphi$, when $M$ is a Kripke structure, incorporates the universal quantification over the paths originating from the initial states of $M$.
Consider a Kripke structure $M$ with states ${0,1,2}$, initial states ${0}$, and the following transition relation,
$$ {(0,1),(0,2),(1,2),(2,2)} enspace. $$
Suppose that the atomic proposition $p$ holds at states $0$ and $2$. Then we have $M models mathsf{F} p$, but $M notmodels mathsf{G} p$. If $pi_1$ is the path $0,1,2,2,ldots$ and $pi_2$ is the path $0,2,2,ldots$, then $pi_2 models mathsf{G} p$, but $pi_1 notmodels mathsf{G} p$; hence $M notmodels mathsf{G} p$.
answered Jan 6 at 14:40
Fabio SomenziFabio Somenzi
6,41321221
$endgroup$
add a comment |
$begingroup$
$mathsf{G}$ is a temporal operator (or modality). $pi models mathsf{G} p$ means that $p$ holds at all states of path $pi$.
$mathsf{A}$ is a path quantifier. In CTL and CTL$^*$, $mathsf A$ quantifies over all the paths originating from a state. In LTL it is as if there were an implicit $mathsf A$ in front of the whole formula. In fact, to translate from LTL to CTL$^*$, one simply adds an $mathsf{A}$ in front of the LTL formula.
The first example you gave, $M models mathsf{AG,EF} ,p$, concerns a CTL formula that says that from all states of $M$ reachable from the initial states of $M$ there originates a path along which $p$ eventually holds. (This property is often called resetability, because $p$ may be chosen to distinguish the reset states of the model.)
The second example you gave, $M models mathsf{A,EF} ,p$, concerns a CTL$^*$ formula equivalent to $mathsf{EF} ,p$. $M$ satisfies $mathsf{EF} ,p$ if, from all initial states of $M$, a state where $p$ holds is reachable.
Neither example is expressible in LTL. Both require branching time.
Perhaps, the CTL (and CTL$^*$) formula $mathsf{AG} ,p$ illustrates the difference between $mathsf{A}$ and $mathsf{G}$ best. In English, $M,s modelsmathsf{AG} ,p$ says "along all states of all paths of $M$ originating from state $s$, $p$ holds." Both $mathsf{A}$ and $mathsf{G}$ are necessary in CTL to express that $p$ is invariant in $M$.
In LTL one simply skips the initial (implicit) $mathsf A$, because the definition of $M models varphi$, when $M$ is a Kripke structure, incorporates the universal quantification over the paths originating from the initial states of $M$.
Consider a Kripke structure $M$ with states ${0,1,2}$, initial states ${0}$, and the following transition relation,
$$ {(0,1),(0,2),(1,2),(2,2)} enspace. $$
Suppose that the atomic proposition $p$ holds at states $0$ and $2$. Then we have $M models mathsf{F} p$, but $M notmodels mathsf{G} p$. If $pi_1$ is the path $0,1,2,2,ldots$ and $pi_2$ is the path $0,2,2,ldots$, then $pi_2 models mathsf{G} p$, but $pi_1 notmodels mathsf{G} p$; hence $M notmodels mathsf{G} p$.
answered Jan 6 at 14:40
Fabio SomenziFabio Somenzi
6,41321221
$endgroup$
add a comment |
$begingroup$
$mathsf{G}$ is a temporal operator (or modality). $pi models mathsf{G} p$ means that $p$ holds at all states of path $pi$.
$mathsf{A}$ is a path quantifier. In CTL and CTL$^*$, $mathsf A$ quantifies over all the paths originating from a state. In LTL it is as if there were an implicit $mathsf A$ in front of the whole formula. In fact, to translate from LTL to CTL$^*$, one simply adds an $mathsf{A}$ in front of the LTL formula.
The first example you gave, $M models mathsf{AG,EF} ,p$, concerns a CTL formula that says that from all states of $M$ reachable from the initial states of $M$ there originates a path along which $p$ eventually holds. (This property is often called resetability, because $p$ may be chosen to distinguish the reset states of the model.)
The second example you gave, $M models mathsf{A,EF} ,p$, concerns a CTL$^*$ formula equivalent to $mathsf{EF} ,p$. $M$ satisfies $mathsf{EF} ,p$ if, from all initial states of $M$, a state where $p$ holds is reachable.
Neither example is expressible in LTL. Both require branching time.
Perhaps, the CTL (and CTL$^*$) formula $mathsf{AG} ,p$ illustrates the difference between $mathsf{A}$ and $mathsf{G}$ best. In English, $M,s modelsmathsf{AG} ,p$ says "along all states of all paths of $M$ originating from state $s$, $p$ holds." Both $mathsf{A}$ and $mathsf{G}$ are necessary in CTL to express that $p$ is invariant in $M$.
In LTL one simply skips the initial (implicit) $mathsf A$, because the definition of $M models varphi$, when $M$ is a Kripke structure, incorporates the universal quantification over the paths originating from the initial states of $M$.
Consider a Kripke structure $M$ with states ${0,1,2}$, initial states ${0}$, and the following transition relation,
$$ {(0,1),(0,2),(1,2),(2,2)} enspace. $$
Suppose that the atomic proposition $p$ holds at states $0$ and $2$. Then we have $M models mathsf{F} p$, but $M notmodels mathsf{G} p$. If $pi_1$ is the path $0,1,2,2,ldots$ and $pi_2$ is the path $0,2,2,ldots$, then $pi_2 models mathsf{G} p$, but $pi_1 notmodels mathsf{G} p$; hence $M notmodels mathsf{G} p$.
answered Jan 6 at 14:40
Fabio SomenziFabio Somenzi
6,41321221
$endgroup$
$mathsf{G}$ is a temporal operator (or modality). $pi models mathsf{G} p$ means that $p$ holds at all states of path $pi$.
$mathsf{A}$ is a path quantifier. In CTL and CTL$^*$, $mathsf A$ quantifies over all the paths originating from a state. In LTL it is as if there were an implicit $mathsf A$ in front of the whole formula. In fact, to translate from LTL to CTL$^*$, one simply adds an $mathsf{A}$ in front of the LTL formula.
The first example you gave, $M models mathsf{AG,EF} ,p$, concerns a CTL formula that says that from all states of $M$ reachable from the initial states of $M$ there originates a path along which $p$ eventually holds. (This property is often called resetability, because $p$ may be chosen to distinguish the reset states of the model.)
The second example you gave, $M models mathsf{A,EF} ,p$, concerns a CTL$^*$ formula equivalent to $mathsf{EF} ,p$. $M$ satisfies $mathsf{EF} ,p$ if, from all initial states of $M$, a state where $p$ holds is reachable.
Neither example is expressible in LTL. Both require branching time.
Perhaps, the CTL (and CTL$^*$) formula $mathsf{AG} ,p$ illustrates the difference between $mathsf{A}$ and $mathsf{G}$ best. In English, $M,s modelsmathsf{AG} ,p$ says "along all states of all paths of $M$ originating from state $s$, $p$ holds." Both $mathsf{A}$ and $mathsf{G}$ are necessary in CTL to express that $p$ is invariant in $M$.
In LTL one simply skips the initial (implicit) $mathsf A$, because the definition of $M models varphi$, when $M$ is a Kripke structure, incorporates the universal quantification over the paths originating from the initial states of $M$.
Consider a Kripke structure $M$ with states ${0,1,2}$, initial states ${0}$, and the following transition relation,
$$ {(0,1),(0,2),(1,2),(2,2)} enspace. $$
Suppose that the atomic proposition $p$ holds at states $0$ and $2$. Then we have $M models mathsf{F} p$, but $M notmodels mathsf{G} p$. If $pi_1$ is the path $0,1,2,2,ldots$ and $pi_2$ is the path $0,2,2,ldots$, then $pi_2 models mathsf{G} p$, but $pi_1 notmodels mathsf{G} p$; hence $M notmodels mathsf{G} p$.
answered Jan 6 at 14:40
Fabio SomenziFabio Somenzi
6,41321221
edited Jan 6 at 16:08
answered Jan 6 at 14:40
Fabio SomenziFabio Somenzi
6,41321221
answered Jan 6 at 14:40
Fabio SomenziFabio Somenzi
6,41321221
answered Jan 6 at 14:40
Fabio SomenziFabio Somenzi
6,41321221
6,41321221
add a comment |
add a comment |
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3063882%2fi-dont-understand-the-g-syntax-in-a-ltl-linear-temporal-logic-formula%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
1
$begingroup$
See LTL.
$endgroup$
– Mauro ALLEGRANZA
Jan 6 at 13:58
$begingroup$
@MauroALLEGRANZA Where do you think I got literally my first scentence from? What does it mean to "Globally: φ has to hold on the entire subsequent path." That all states have L(state) = φ?
$endgroup$
– Felix Rosén
Jan 6 at 14:01