{ "labelLang" : "eng", "responseDate" : "2024-03-29 09:38", "paging" : { "last" : true, "first" : true, "totalPages" : 1, "totalElements" : 27, "totalUncutElements" : 27, "totalEstimatedElements" : 10, "size" : 100, "number" : 1, "numberOfElements" : 27, "sort" : [ { "direction" : "DESC", "property" : "publishedYear", "ascending" : false }, { "direction" : "ASC", "property" : "firstAuthor", "ascending" : true }, { "direction" : "ASC", "property" : "title", "ascending" : true } ] }, "content" : [ { "otype" : "JournalArticle", "mtid" : 34609659, "status" : "VALIDATED", "published" : true, "unhandledTickets" : 0, "deleted" : false, "lastRefresh" : "2024-02-17T14:02:41.204+0000", "lastModified" : "2024-02-17T14:01:19.073+0000", "created" : "2024-02-17T14:01:18.074+0000", "creator" : { "otype" : "Admin", "mtid" : 521, "link" : "/api/admin/521", "label" : "Admin Szuper (admin)", "familyName" : "Szuper", "givenName" : "Admin", "published" : true, "snippet" : true }, "lastDuplumSearch" : "2024-02-19T08:56:44.256+0000", "validated" : "2024-02-17T14:01:18.325+0000", "validator" : { "otype" : "Admin", "mtid" : 521, "link" : "/api/admin/521", "label" : "Admin Szuper (admin)", "familyName" : "Szuper", "givenName" : "Admin", "published" : true, "snippet" : true }, "core" : false, "citation" : true, "publicationPending" : false, "type" : { "otype" : "PublicationType", "mtid" : 24, "link" : "/api/publicationtype/24", "label" : "Journal Article", "code" : 24, "otypeName" : "JournalArticle", "listPosition" : 1, "published" : true, "oldId" : 24, "snippet" : true }, "subType" : { "otype" : "SubType", "mtid" : 10000059, "link" : "/api/subtype/10000059", "label" : "Article (Journal Article)", "name" : "Szakcikk", "nameEng" : "Article", "docType" : { "otype" : "PublicationType", "mtid" : 24, "link" : "/api/publicationtype/24", "label" : "Journal Article", "code" : 24, "otypeName" : "JournalArticle", "listPosition" : 1, "published" : true, "oldId" : 24, "snippet" : true }, "listPosition" : 101, "published" : true, "oldId" : 10000059, "snippet" : true }, "category" : { "otype" : "Category", "mtid" : 1, "link" : "/api/category/1", "label" : "Scientific", "published" : true, "oldId" : 1, "snippet" : true }, "languages" : [ { "otype" : "Language", "mtid" : 10002, "link" : "/api/language/10002", "label" : "English", "name" : "Angol", "nameEng" : "English", "published" : true, "oldId" : 2, "snippet" : true } ], "firstAuthor" : "Schneider, Sven", "authorships" : [ { "otype" : "PersonAuthorship", "mtid" : 114659384, "link" : "/api/authorship/114659384", "label" : "Schneider, Sven ✉", "listPosition" : 1, "share" : 0.33333334, "first" : true, "last" : false, "corresponding" : true, "familyName" : "Schneider", "givenName" : "Sven", "authorTyped" : true, "editorTyped" : false, "otherTyped" : false, "type" : { "otype" : "AuthorshipType", "mtid" : 1, "link" : "/api/authorshiptype/1", "label" : "Author", "code" : 0, "published" : true, "oldId" : 0, "snippet" : true }, "published" : false, "snippet" : true }, { "otype" : "PersonAuthorship", "mtid" : 114659385, "link" : "/api/authorship/114659385", "label" : "Maximova, Maria", "listPosition" : 2, "share" : 0.33333334, "first" : false, "last" : false, "corresponding" : false, "familyName" : "Maximova", "givenName" : "Maria", "authorTyped" : true, "editorTyped" : false, "otherTyped" : false, "type" : { "otype" : "AuthorshipType", "mtid" : 1, "link" : "/api/authorshiptype/1", "label" : "Author", "code" : 0, "published" : true, "oldId" : 0, "snippet" : true }, "published" : false, "snippet" : true }, { "otype" : "PersonAuthorship", "mtid" : 114659386, "link" : "/api/authorship/114659386", "label" : "Giese, Holger", "listPosition" : 3, "share" : 0.33333334, "first" : false, "last" : true, "corresponding" : false, "familyName" : "Giese", "givenName" : "Holger", "authorTyped" : true, "editorTyped" : false, "otherTyped" : false, "type" : { "otype" : "AuthorshipType", "mtid" : 1, "link" : "/api/authorshiptype/1", "label" : "Author", "code" : 0, "published" : true, "oldId" : 0, "snippet" : true }, "published" : false, "snippet" : true } ], "title" : "Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic", "identifiers" : [ { "otype" : "PublicationIdentifier", "mtid" : 25560986, "link" : "/api/publicationidentifier/25560986", "label" : "DOI: 10.1016/j.jlamp.2023.100938", "source" : { "otype" : "PlainSource", "mtid" : 6, "link" : "/api/publicationsource/6", "label" : "DOI", "type" : { "otype" : "PublicationSourceType", "mtid" : 10001, "link" : "/api/publicationsourcetype/10001", "label" : "DOI", "mayHaveOa" : true, "published" : true, "snippet" : true }, "name" : "DOI", "nameEng" : "DOI", "linkPattern" : "https://doi.org/@@@", "publiclyVisible" : true, "published" : true, "oldId" : 6, "snippet" : true }, "idValue" : "10.1016/j.jlamp.2023.100938", "realUrl" : "https://doi.org/10.1016/j.jlamp.2023.100938", "published" : false, "snippet" : true }, { "otype" : "PublicationIdentifier", "mtid" : 25560985, "link" : "/api/publicationidentifier/25560985", "label" : "WoS: 001142843300001", "source" : { "otype" : "PlainSource", "mtid" : 1, "link" : "/api/publicationsource/1", "label" : "WoS", "type" : { "otype" : "PublicationSourceType", "mtid" : 10003, "link" : "/api/publicationsourcetype/10003", "label" : "Indexelő adatbázis", "mayHaveOa" : false, "published" : true, "snippet" : true }, "name" : "WoS", "nameEng" : "WoS", "linkPattern" : "https://www.webofscience.com/wos/woscc/full-record/@@@", "publiclyVisible" : true, "published" : true, "oldId" : 1, "snippet" : true }, "validState" : "IDENTICAL", "idValue" : "001142843300001", "realUrl" : "https://www.webofscience.com/wos/woscc/full-record/001142843300001", "published" : false, "snippet" : true } ], "journal" : { "otype" : "Journal", "mtid" : 10044317, "link" : "/api/journal/10044317", "label" : "JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING 2352-2208 2352-2216", "pIssn" : "2352-2208", "eIssn" : "2352-2216", "reviewType" : "REVIEWED", "noIF" : false, "sciIndexed" : true, "scopusIndexed" : true, "lang" : "FOREIGN", "hungarian" : false, "published" : true, "oldId" : 10044317, "snippet" : true }, "volume" : "137", "internalId" : "100938", "firstPageOrInternalIdForSort" : "100938", "pageLength" : 48, "publishedYear" : 2024, "abstractText" : "Cyber-physical systems often encompass complex concurrent behavior with timing constraints and probabilistic failures on demand. The analysis whether such systems with probabilistic timed behavior adhere to a given specification is essential. The formalism of Interval Probabilistic Timed Graph Transformation Systems (IPTGTSs) is often a suitable choice to model cyber-physical systems because (a) its rule-based approach to graph transformation can capture a wide range of system's structure dynamics when the states of the system can be represented by graphs while (b) it employs interval specifications for probabilistic behavior as well as lower and upper bounds on delays of steps to support systems where precise probabilities and delays are not known or may change during the runtime of the system. Probabilistic Metric Temporal Graph Logic (PMTGL) has been introduced as a powerful specification language to express worst-case/best-case probabilistic timed requirements such as actor-based soft deadlines using (a) path properties relying on its Metric Temporal Graph Logic fragment to track individual graph elements and (b) an operator inherited from Probabilistic Timed Computation Tree Logic to express worst-case/best-case probabilistic requirements identifying worst-case/best-case resolutions of non-determinism. Bounded Model Checking (BMC) support for Probabilistic Timed Graph Transformation Systems (PTGTSs) w.r.t. properties specified using PMTGL has been already presented. However, for IPTGTSs no analysis support w.r.t. PMTGL properties has been developed for stating metric temporal properties on identified subgraphs and their structural changes over time.In this paper, we adapt the BMC approach developed for PTGTSs to the case of IPTGTSs extending modeling and analysis support to the usage of probability intervals more appropriately covering cyber-physical systems where probabilistic effects cannot be specified precisely and need to be approximated instead. In our evaluation, we apply an implementation of our BMC approach in AUTOGRAPH to a novel running example demonstrating the effect of using probability intervals instead of precise probability values.", "subjects" : [ { "otype" : "Classification", "mtid" : 10003, "link" : "/api/classification/10003", "label" : "Mathematics", "published" : true, "snippet" : true }, { "otype" : "Classification", "mtid" : 10034, "link" : "/api/classification/10034", "label" : "Computer and information sciences", "published" : true, "snippet" : true } ], "keywords" : [ { "otype" : "Keyword", "mtid" : 5767, "link" : "/api/keyword/5767", "label" : "quantitative analysis", "published" : true, "oldId" : 5767, "snippet" : true }, { "otype" : "Keyword", "mtid" : 1000454, "link" : "/api/keyword/1000454", "label" : "qualitative analysis", "published" : true, "oldId" : 1000454, "snippet" : true }, { "otype" : "Keyword", "mtid" : 1326334, "link" : "/api/keyword/1326334", "label" : "Cyber-physical systems", "published" : true, "oldId" : 1326334, "snippet" : true }, { "otype" : "Keyword", "mtid" : 1694131, "link" : "/api/keyword/1694131", "label" : "Bounded Model Checking", "published" : true, "snippet" : true }, { "otype" : "Keyword", "mtid" : 2805361, "link" : "/api/keyword/2805361", "label" : "probabilistic timed systems", "published" : true, "snippet" : true } ], "digital" : null, "printed" : null, "sourceYear" : 2024, "foreignEdition" : true, "foreignLanguage" : true, "fullPublication" : true, "conferencePublication" : false, "nationalOrigin" : null, "missingAuthor" : false, "oaType" : "NONE", "oaCheckDate" : "2024-02-17", "oaFree" : false, "citationCount" : 0, "citationCountUnpublished" : 0, "citationCountWoOther" : 0, "independentCitCountWoOther" : 0, "doiCitationCount" : 0, "wosCitationCount" : 0, "scopusCitationCount" : 0, "independentCitationCount" : 0, "unhandledCitationCount" : 0, "citingPubCount" : 0, "independentCitingPubCount" : 0, "unhandledCitingPubCount" : 0, "citedPubCount" : 1, "citedCount" : 1, "ratings" : [ { "otype" : "MtaRating", "mtid" : 11509176, "link" : "/api/mtarating/11509176", "label" : "IX. Politikatudományi Bizottság:A nemzetközi JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING 2352-2208 2352-2216", "ratingType" : { "otype" : "RatingType", "mtid" : 10015, "link" : "/api/ratingtype/10015", "label" : "IX. Politikatudományi Bizottság", "code" : "PTB", "institute" : { "otype" : "Institute", "mtid" : 14099, "link" : "/api/institute/14099", "label" : "Politikatudományi Bizottság HASSELIX PTB [1901-]", "childrenCount" : 0, "allowInstForum" : false, "allowOnlineRegistration" : true, "name" : "Politikatudományi Bizottság", "nameEng" : "Politikatudományi Bizottság", "published" : true, "oldId" : 14099, "snippet" : true }, "published" : true, "snippet" : true }, "val" : "A nemzetközi", "published" : false, "snippet" : true }, { "otype" : "SjrRating", "mtid" : 11453598, "link" : "/api/sjrrating/11453598", "label" : "sjr:D1 (2024) Scopus - Cultural Studies JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING 2352-2208 2352-2216", "listPos" : 115, "rankValue" : 0.1, "type" : "journal", "ratingType" : { "otype" : "RatingType", "mtid" : 10002, "link" : "/api/ratingtype/10002", "label" : "sjr", "code" : "sjr", "published" : true, "snippet" : true }, "subject" : { "otype" : "ClassificationExternal", "mtid" : 3316, "link" : "/api/classificationexternal/3316", "label" : "Scopus - Cultural Studies", "published" : true, "oldId" : 3316, "snippet" : true }, "ranking" : "D1", "calculation" : "FROM_PREVIOUS_TO_LAST_YEAR", "published" : true, "snippet" : true } ], "ratingsForSort" : "D1", "mtaRatingsForSort" : "A nemzetközi", "hasCitationDuplums" : false, "directInstitutesForSort" : "", "ownerAuthorCount" : 1, "ownerInstituteCount" : 3, "directInstituteCount" : 0, "authorCount" : 3, "contributorCount" : 0, "hasQualityFactor" : true, "link" : "/api/publication/34609659", "label" : "Schneider Sven et al. Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic. (2024) JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING 2352-2208 2352-2216 137", "template" : "