In theoretical computer science, the modal μ-calculus (Lμ, Lμ, sometimes just μ-calculus, although this can have a more general meaning) is an extension of propositional modal logic (with many modalities) by adding the least fixed point operator μ and the greatest fixed point operator ν, thus a fixed-point logic.
| Attributes | Values |
|---|
| rdfs:label
| - Modal μ-calculus (en)
- Μ λογισμός (el)
- Mu-calcul (fr)
|
| rdfs:comment
| - Ο μ-λογισμός (ή τροπικός μ λογισμός) είναι μια επέκταση της προτασιακής τροπικής λογικής με έναν τελεστή μ ελάχιστου σταθερού σημείου (fixpoint). Χρησιμοποιείται για να περιγράψει τις ιδιότητες των συστημάτων μεταβάσεων με ετικέτες και να τις επαληθεύσει. Ο (προτασιακός) μ-λογισμός εφευρέθηκε από τον Ντέινα Σκοτ και τον Τζάκο ντε Μπέκερ, και στη συνέχεια αναπτύχθηκε από τον Ντέξτερ Κόζεν για να φτάσει στην έκδοση που χρησιμοποιείται σήμερα. Πολλές χρονικές λογικές μπορούν να κωδικοποιηθούν στο μ-λογισμό, όπως η LTL, η CTL και η CTL*. (el)
- In theoretical computer science, the modal μ-calculus (Lμ, Lμ, sometimes just μ-calculus, although this can have a more general meaning) is an extension of propositional modal logic (with many modalities) by adding the least fixed point operator μ and the greatest fixed point operator ν, thus a fixed-point logic. (en)
- En logique mathématique et en informatique théorique, le mu-calcul (ou logique du mu-calcul modal) est l'extension de la logique modale classique avec des opérateurs de points fixes. Selon Bradfield et Walukiewicz, le mu-calcul est une des logiques les plus importantes pour la vérification de modèles ; elle est expressive tout en ayant de bonnes propriétés algorithmiques. (fr)
|
| dcterms:subject
| |
| Wikipage page ID
| |
| Wikipage revision ID
| |
| Link from a Wikipage to another Wikipage
| |
| Link from a Wikipage to an external page
| |
| sameAs
| |
| dbp:wikiPageUsesTemplate
| |
| has abstract
| - Ο μ-λογισμός (ή τροπικός μ λογισμός) είναι μια επέκταση της προτασιακής τροπικής λογικής με έναν τελεστή μ ελάχιστου σταθερού σημείου (fixpoint). Χρησιμοποιείται για να περιγράψει τις ιδιότητες των συστημάτων μεταβάσεων με ετικέτες και να τις επαληθεύσει. Ο (προτασιακός) μ-λογισμός εφευρέθηκε από τον Ντέινα Σκοτ και τον Τζάκο ντε Μπέκερ, και στη συνέχεια αναπτύχθηκε από τον Ντέξτερ Κόζεν για να φτάσει στην έκδοση που χρησιμοποιείται σήμερα. Πολλές χρονικές λογικές μπορούν να κωδικοποιηθούν στο μ-λογισμό, όπως η LTL, η CTL και η CTL*. (el)
- En logique mathématique et en informatique théorique, le mu-calcul (ou logique du mu-calcul modal) est l'extension de la logique modale classique avec des opérateurs de points fixes. Selon Bradfield et Walukiewicz, le mu-calcul est une des logiques les plus importantes pour la vérification de modèles ; elle est expressive tout en ayant de bonnes propriétés algorithmiques. Le mu-calcul (propositionnel et modal) a d'abord été introduit par Dana Scott et Jaco de Bakker puis a été étendu dans sa version moderne par Dexter Kozen. Cette logique permet de décrire les propriétés des systèmes de transition d'états et de les vérifier. De nombreuses logiques temporelles (telles que CTL* ou ses fragments très usités comme (en) ou LTL) sont des fragments du mu-calcul. Une manière algébrique de voir le mu-calcul est de le considérer comme une algèbre de fonctions monotones sur un treillis complet, les opérateurs étant une composition fonctionnelle plus des points fixes ; de ce point de vue, le mu-calcul agit sur le treillis de l'algèbre des ensembles. La sémantique des jeux du mu-calcul est liée aux jeux à deux joueurs à information parfaite, notamment les jeux de parité. (fr)
- In theoretical computer science, the modal μ-calculus (Lμ, Lμ, sometimes just μ-calculus, although this can have a more general meaning) is an extension of propositional modal logic (with many modalities) by adding the least fixed point operator μ and the greatest fixed point operator ν, thus a fixed-point logic. The (propositional, modal) μ-calculus originates with Dana Scott and Jaco de Bakker, and was further developed by Dexter Kozen into the version most used nowadays. It is used to describe properties of labelled transition systems and for verifying these properties. Many temporal logics can be encoded in the μ-calculus, including CTL* and its widely used fragments—linear temporal logic and computational tree logic. An algebraic view is to see it as an algebra of monotonic functions over a complete lattice, with operators consisting of functional composition plus the least and greatest fixed point operators; from this viewpoint, the modal μ-calculus is over the lattice of a power set algebra. The game semantics of μ-calculus is related to two-player games with perfect information, particularly infinite parity games. (en)
|
| prov:wasDerivedFrom
| |
| page length (characters) of wiki page
| |
| foaf:isPrimaryTopicOf
| |
| is Link from a Wikipage to another Wikipage
of | |
| is Wikipage redirect
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)