Computation tree logic (original) (raw)
Η λογική υπολογιστικού δένδρου (Computation tree logic, CTL) είναι μια λογική διακλαδιζόμενου χρόνου (branching-time), το οποίο σημαίνει ότι το μοντέλο της για το χρόνο είναι μια δενδρική δομή, στην οποία το μέλλον δεν έχει οριστεί αλλά υπάρχουν διαφορετικά μονοπάτια σε αυτό και κάθε ένα από αυτά τα μονοπάτια μπορεί να είναι ένα μονοπάτι που θα πραγματοποιηθεί. Χρησιμοποιείται στην τυπική επαλήθευση λογισμικού ή υλικού, συνήθως από λογισμικό που ονομάζεται ελεγκτής μοντέλων. Το λογισμικό αυτό προσδιορίζει αν το λογισμικό ή το υλικό που ελέγχεται έχει κάποιες συγκεκριμένες ιδιότητες ασφάλειας (safety) ή ζωτικότητας (liveness). Ανήκει στην κατηγορία των χρονικών λογικών, όπως και η γραμμική χρονική λογική.
| Property | Value |
|---|---|
| dbo:abstract | Η λογική υπολογιστικού δένδρου (Computation tree logic, CTL) είναι μια λογική διακλαδιζόμενου χρόνου (branching-time), το οποίο σημαίνει ότι το μοντέλο της για το χρόνο είναι μια δενδρική δομή, στην οποία το μέλλον δεν έχει οριστεί αλλά υπάρχουν διαφορετικά μονοπάτια σε αυτό και κάθε ένα από αυτά τα μονοπάτια μπορεί να είναι ένα μονοπάτι που θα πραγματοποιηθεί. Χρησιμοποιείται στην τυπική επαλήθευση λογισμικού ή υλικού, συνήθως από λογισμικό που ονομάζεται ελεγκτής μοντέλων. Το λογισμικό αυτό προσδιορίζει αν το λογισμικό ή το υλικό που ελέγχεται έχει κάποιες συγκεκριμένες ιδιότητες ασφάλειας (safety) ή ζωτικότητας (liveness). Ανήκει στην κατηγορία των χρονικών λογικών, όπως και η γραμμική χρονική λογική. (el) Computation tree logic (CTL) is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realized. It is used in formal verification of software or hardware artifacts, typically by software applications known as model checkers, which determine if a given artifact possesses safety or liveness properties. For example, CTL can specify that when some initial condition is satisfied (e.g., all program variables are positive or no cars on a highway straddle two lanes), then all possible executions of a program avoid some undesirable condition (e.g., dividing a number by zero or two cars colliding on a highway). In this example, the safety property could be verified by a model checker that explores all possible transitions out of program states satisfying the initial condition and ensures that all such executions satisfy the property. Computation tree logic belongs to a class of temporal logics that includes linear temporal logic (LTL). Although there are properties expressible only in CTL and properties expressible only in LTL, all properties expressible in either logic can also be expressed in CTL*. CTL was first proposed by Edmund M. Clarke and E. Allen Emerson in 1981, who used it to synthesize so-called synchronisation skeletons, i.e abstractions of concurrent programs. (en) Die Computation Tree Logic (kurz CTL) ist eine Temporale Logik, deren Modell der Zeit eine baumartige Struktur hat. Die zeitliche Änderung von Zuständen und deren Eigenschaften wird durch Pfade innerhalb dieser Baumstruktur modelliert. Hierbei hat die Zukunft mehrere Pfade, wobei nicht festgelegt ist, welche letztendlich realisiert werden. Demnach können Aussagen über die mögliche Entwicklungen getroffen werden. Die CTL wird zur Verifikation von Hard- und Software verwendet, üblicherweise von Model Checkern. Zu der Familie der temporalen Logiken gehört auch die Linear temporale Logik (LTL), wobei hier nur eine Zukunft möglich ist. Eine Verallgemeinerung der beiden Logiken wird als CTL* bezeichnet. (de) 計算木論理（けいさんきろんり、Computational Tree Logic、CTL）は、分岐時相論理の一種である。その時間モデルでは未来は決定されておらず木構造のように分岐している。未来の複数の経路のうちの1つが実際に現実の経路となる。 (ja) 계산 트리 논리 또는 계산 나무 논리(Computational Tree Logic, CTL)은 의 한 종류로, 어떤 상태에서 실행이 가능한 상태로의 경로를 트리 구조로 전개한 결과인 계산 트리와 의미론이 정의된 논리 체계이다. CTL에서는 에서 사용되는 시간 연산자인 F, G, X, U, R 외에 '모든 실행 가능한 경로에 대해'를 의미하는 A, '어떤 실행가능한 경로에 대해'를 의미하는 E가 포함되어 사용된다. (ko) Logika CTL – jedna z logik temporalnych. Jest oparta na liniowej strukturze czasu. (pl) Lógica de Árvore de Computação (LAC) é uma ramificação-temporal da Lógica, significando que seu modelo de tempo é como a estrutura árvore no qual o futuro não é determinado. Não tem caminhos diferentes no futuro, qualquer um deles pode ser um caminho atual que é realizado. É usado na verificação formal de artefatos de software ou hardware, tipicamente por aplicações de software conhecidas como verificadores de modelos que determina se um dado artefato possui propriedades de segurança ou liveness. Por exemplo, LAC pode especificar que quando alguma condição inicial é satisfeita (ex: todas as variáveis do programa são positivas ou não há carros na estrada que escarrancham duas pistas ), então todas as possíveis execuções do programa evitam alguma condição indesejável (ex: dividir um número por zero ou o a colisão de dois carros na estrada) . Neste exemplo, a propriedade de segurança pode ser verificada por um modelo verificador que explora todas as possibilidades de transações para fora de um programa de estados satisfazendo a condição inicial que garante que todos as execuções satisfazem esta propriedade. Lógica de Árvore de Computação está na classe de Lógica temporal que inclui Lógica Temporal (LLT). Embora aqui existam propriedades expressáveis em apenas uma das LAC ou LLT, todas as propriedades em ambas as lógicas podem ser expressas em . (pt) Lógica de Árvore de Computação (LAC) é uma ramificação-temporal da Lógica, significando que seu modelo de tempo é como a estrutura árvore no qual o futuro não é determinado. Não tem caminhos diferentes no futuro, qualquer um deles pode ser um caminho atual que é realizado. É usado na verificação formal de artefatos de software ou hardware, tipicamente por aplicações de software conhecidas como verificadores de modelos que determina se um dado artefato possui propriedades de segurança ou liveness. Por exemplo, ALC pode especificar que quando alguma condição inicial é satisfeita (ex: todas as variáveis do programa são positivas ou não há carros na estrada que escarrancham duas pistas ), então todas as possíveis execuções do programa evitam alguma condição indesejável (ex: dividir um número por zero ou o a colisão de dois carros na estrada) . Neste exemplo, a propriedade de segurança pode ser verificada por um modelo verificador que explora todas as possibilidades de transações para fora de um programa de estados satisfazendo a condição inicial que garante que todos as execuções satisfazem esta propriedade. Árvore Lógica Computacional está na classe de Lógica temporal que inclui Lógica Temporal (LLT). Embora aqui existam propriedades expressáveis em apenas uma das ALC ou LLT, todas as propriedades em ambas as lógicas podem ser expressas em . (pt) |
| dbo:wikiPageExternalLink | http://www.inf.unibz.it/~artale/FM/slide4.pdf https://www.cs.cmu.edu/afs/cs/user/emc/www/papers/Invited%20Conference%20Articles/Design%20and%20Synthesis%20of%20Synchronization%20Skeletons%20Using%20Branching%20Time%20Temporal%20Logic.pdf |
| dbo:wikiPageID | 840894 (xsd:integer) |
| dbo:wikiPageLength | 17529 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1113052654 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:De_Morgan's_laws dbr:PSPACE-complete dbr:Context-free_grammar dbr:Mathematical_logic dbr:Safety_and_Liveness_Properties dbr:Graph_(discrete_mathematics) dbr:Model_checking dbr:Regular_Language dbr:Logical_operator dbr:Time dbr:Tree_(graph_theory) dbr:Truth dbr:Linear_temporal_logic dbr:E._Allen_Emerson dbr:Edmund_M._Clarke dbr:Alternating-time_temporal_logic dbr:False_(logic) dbr:First-order_logic dbr:Formal_verification dbr:Fair_computational_tree_logic dbr:Entailment dbr:Logical_connective dbr:Well-formed_formula dbr:Atomic_formula dbr:Temporal_logic dbc:Logic_in_computer_science dbc:Automata_(computation) dbr:Transition_system dbr:CTL* dbc:Temporal_logic dbr:Monadic_second-order_logic dbr:Undecidable_problem dbr:Probabilistic_CTL dbr:Model_checker dbr:Concurrent_program dbr:Modal_mu_calculus dbr:Well_formed_formula |
| dbp:wikiPageUsesTemplate | dbt:Cite_book dbt:Cite_journal dbt:More_footnotes dbt:Reflist |
| dct:subject | dbc:Logic_in_computer_science dbc:Automata_(computation) dbc:Temporal_logic |
| gold:hypernym | dbr:Logic |
| rdfs:comment | Η λογική υπολογιστικού δένδρου (Computation tree logic, CTL) είναι μια λογική διακλαδιζόμενου χρόνου (branching-time), το οποίο σημαίνει ότι το μοντέλο της για το χρόνο είναι μια δενδρική δομή, στην οποία το μέλλον δεν έχει οριστεί αλλά υπάρχουν διαφορετικά μονοπάτια σε αυτό και κάθε ένα από αυτά τα μονοπάτια μπορεί να είναι ένα μονοπάτι που θα πραγματοποιηθεί. Χρησιμοποιείται στην τυπική επαλήθευση λογισμικού ή υλικού, συνήθως από λογισμικό που ονομάζεται ελεγκτής μοντέλων. Το λογισμικό αυτό προσδιορίζει αν το λογισμικό ή το υλικό που ελέγχεται έχει κάποιες συγκεκριμένες ιδιότητες ασφάλειας (safety) ή ζωτικότητας (liveness). Ανήκει στην κατηγορία των χρονικών λογικών, όπως και η γραμμική χρονική λογική. (el) 計算木論理（けいさんきろんり、Computational Tree Logic、CTL）は、分岐時相論理の一種である。その時間モデルでは未来は決定されておらず木構造のように分岐している。未来の複数の経路のうちの1つが実際に現実の経路となる。 (ja) 계산 트리 논리 또는 계산 나무 논리(Computational Tree Logic, CTL)은 의 한 종류로, 어떤 상태에서 실행이 가능한 상태로의 경로를 트리 구조로 전개한 결과인 계산 트리와 의미론이 정의된 논리 체계이다. CTL에서는 에서 사용되는 시간 연산자인 F, G, X, U, R 외에 '모든 실행 가능한 경로에 대해'를 의미하는 A, '어떤 실행가능한 경로에 대해'를 의미하는 E가 포함되어 사용된다. (ko) Logika CTL – jedna z logik temporalnych. Jest oparta na liniowej strukturze czasu. (pl) Die Computation Tree Logic (kurz CTL) ist eine Temporale Logik, deren Modell der Zeit eine baumartige Struktur hat. Die zeitliche Änderung von Zuständen und deren Eigenschaften wird durch Pfade innerhalb dieser Baumstruktur modelliert. Hierbei hat die Zukunft mehrere Pfade, wobei nicht festgelegt ist, welche letztendlich realisiert werden. Demnach können Aussagen über die mögliche Entwicklungen getroffen werden. Die CTL wird zur Verifikation von Hard- und Software verwendet, üblicherweise von Model Checkern. (de) Computation tree logic (CTL) is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realized. It is used in formal verification of software or hardware artifacts, typically by software applications known as model checkers, which determine if a given artifact possesses safety or liveness properties. For example, CTL can specify that when some initial condition is satisfied (e.g., all program variables are positive or no cars on a highway straddle two lanes), then all possible executions of a program avoid some undesirable condition (e.g., dividing a number by zero or two cars colliding on a highway). In this example, the safety property (en) Lógica de Árvore de Computação (LAC) é uma ramificação-temporal da Lógica, significando que seu modelo de tempo é como a estrutura árvore no qual o futuro não é determinado. Não tem caminhos diferentes no futuro, qualquer um deles pode ser um caminho atual que é realizado. É usado na verificação formal de artefatos de software ou hardware, tipicamente por aplicações de software conhecidas como verificadores de modelos que determina se um dado artefato possui propriedades de segurança ou liveness. Por exemplo, ALC pode especificar que quando alguma condição inicial é satisfeita (ex: todas as variáveis do programa são positivas ou não há carros na estrada que escarrancham duas pistas ), então todas as possíveis execuções do programa evitam alguma condição indesejável (ex: dividir um número p (pt) Lógica de Árvore de Computação (LAC) é uma ramificação-temporal da Lógica, significando que seu modelo de tempo é como a estrutura árvore no qual o futuro não é determinado. Não tem caminhos diferentes no futuro, qualquer um deles pode ser um caminho atual que é realizado. É usado na verificação formal de artefatos de software ou hardware, tipicamente por aplicações de software conhecidas como verificadores de modelos que determina se um dado artefato possui propriedades de segurança ou liveness. Por exemplo, LAC pode especificar que quando alguma condição inicial é satisfeita (ex: todas as variáveis do programa são positivas ou não há carros na estrada que escarrancham duas pistas ), então todas as possíveis execuções do programa evitam alguma condição indesejável (ex: dividir um número p (pt) |
| rdfs:label | Computation tree logic (en) Computation Tree Logic (de) Λογική υπολογιστικού δένδρου (el) 계산 트리 논리 (ko) 計算木論理 (ja) Logika CTL (pl) Árvore Lógica Computacional (pt) Lógica de Árvore de Computação (pt) |
| owl:sameAs | freebase:Computation tree logic wikidata:Computation tree logic wikidata:Computation tree logic dbpedia-de:Computation tree logic dbpedia-el:Computation tree logic dbpedia-fa:Computation tree logic dbpedia-ja:Computation tree logic dbpedia-ko:Computation tree logic dbpedia-pl:Computation tree logic dbpedia-pt:Computation tree logic dbpedia-pt:Computation tree logic https://global.dbpedia.org/id/7G1y |
| prov:wasDerivedFrom | wikipedia-en:Computation_tree_logic?oldid=1113052654&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Computation_tree_logic |
| is dbo:knownFor of | dbr:E._Allen_Emerson |
| is dbo:wikiPageDisambiguates of | dbr:CTL |
| is dbo:wikiPageRedirects of | dbr:Computational_tree_logic dbr:CTL_(logic) |
| is dbo:wikiPageWikiLink of | dbr:List_of_computing_and_IT_abbreviations dbr:Modal_logic dbr:Principles_of_Model_Checking dbr:Infer_Static_Analyzer dbr:List_of_model_checking_tools dbr:Model_checking dbr:Concurrency_(computer_science) dbr:Stuttering_equivalence dbr:Linear_temporal_logic dbr:Linear_time_property dbr:E._Allen_Emerson dbr:Alternating-time_temporal_logic dbr:NuSMV dbr:2-EXPTIME dbr:Temporal_logic dbr:Abstract_model_checking dbr:TAPAAL_Model_Checker dbr:TLA+ dbr:CTL* dbr:Kripke_structure_(model_checking) dbr:CTL dbr:Probabilistic_CTL dbr:Computational_tree_logic dbr:CTL_(logic) |
| is foaf:primaryTopic of | wikipedia-en:Computation_tree_logic |