About: PRISM-games: A model checker for stochastic multi-player games

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: PRISM-games: A model checker for stochastic multi-player games Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
rdfs:seeAlso	http://www.prismmodelchecker.org/papers/tacas13.pdf
Description	We present PRISM-games, a model checker for stochastic multi-player games, which supports modelling, automated verification and strategy synthesis for probabilistic systems with competitive or co-operative behaviour. Models are described in a probabilistic extension of the Reactive Modules language and properties are expressed using rPATL, which extends the well-known logic ATL with operators to reason about probabilities, various reward-based measures, quantitative properties and precise bounds. The tool is based on the probabilistic model checker PRISM, benefiting from its existing user interface and simulator, whilst adding novel model checking algorithms for stochastic games, as well as functionality to synthesise optimal player strategies, explore or export them, and verify other properties under the specified strategy. We present PRISM-games, a model checker for stochastic multi-player games, which supports modelling, automated verification and strategy synthesis for probabilistic systems with competitive or co-operative behaviour. Models are described in a probabilistic extension of the Reactive Modules language and properties are expressed using rPATL, which extends the well-known logic ATL with operators to reason about probabilities, various reward-based measures, quantitative properties and precise bounds. The tool is based on the probabilistic model checker PRISM, benefiting from its existing user interface and simulator, whilst adding novel model checking algorithms for stochastic games, as well as functionality to synthesise optimal player strategies, explore or export them, and verify other properties under the specified strategy. (en)
Title	PRISM-games: A model checker for stochastic multi-player games PRISM-games: A model checker for stochastic multi-player games (en)
skos:prefLabel	PRISM-games: A model checker for stochastic multi-player games PRISM-games: A model checker for stochastic multi-player games (en)
skos:notation	RIV/00216224:14330/13:00068069!RIV14-MSM-14330___
http://linked.open...avai/predkladatel	Fakulta informatiky
http://linked.open...avai/riv/aktivita	I P
http://linked.open...avai/riv/aktivity	I, P(LG13010)
http://linked.open...vai/riv/dodaniDat	2014
http://linked.open...aciTvurceVysledku	Forejt, Vojtěch
http://linked.open.../riv/druhVysledku	D - Článek ve sborníku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Masarykova univerzita / Fakulta informatiky
http://linked.open...dnocenehoVysledku	99534
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/13:00068069
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	model-checker; stochastic games (en)
http://linked.open.../riv/klicoveSlovo	model-checker stochastic games
http://linked.open...ontrolniKodProRIV	[66235D816C64]
http://linked.open...v/mistoKonaniAkce	Rome
http://linked.open...i/riv/mistoVydani	Berlin, Heidelberg
http://linked.open...i/riv/nazevZdroje	TACAS 2013
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	1 (xsd:int)
http://linked.open...cetTvurcuVysledku	5 (xsd:int)
http://linked.open...vavai/riv/projekt	Czech Republic representation in the European Research Consortium for Informatics and Mathematics (ERCIM)
http://linked.open...UplatneniVysledku	2013
http://linked.open...iv/tvurceVysledku	Forejt, Vojtěch Kwiatkowska, Marta Parker, David Chen, Taolue Simaitis, Aistis
http://linked.open...vavai/riv/typAkce	WRD - Světová
http://linked.open.../riv/zahajeniAkce	2013-01-01 (xsd:date)
issn	0302-9743
number of pages	7 (xsd:int)
http://bibframe.org/vocab/doi	10.1007/978-3-642-36742-7_13
http://purl.org/ne...btex#hasPublisher	Springer-Verlag
https://schema.org/isbn	9783642367410
http://localhost/t...ganizacniJednotka	14330

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 85 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software