{ "labelLang" : "hun", "responseDate" : "2024-03-28 16:56", "content" : { "otype" : "JournalArticle", "mtid" : 3025948, "status" : "VALIDATED", "published" : true, "unhandledTickets" : 0, "oldTimestamp" : "2018-02-13T13:55:23.000+0000", "deleted" : false, "oldId" : 3025948, "lastRefresh" : "2024-02-18T08:26:49.650+0000", "lastModified" : "2023-09-19T16:36:39.878+0000", "created" : "2016-02-26T12:11:19.000+0000", "creator" : { "otype" : "Author", "mtid" : 10046994, "link" : "/api/author/10046994", "label" : "Darvas Dániel (Informatika)", "familyName" : "Darvas", "givenName" : "Dániel", "published" : true, "oldId" : 10046994, "snippet" : true }, "lastDuplumOK" : "2023-09-19T16:36:40.134+0000", "lastDuplumSearch" : "2023-09-19T16:36:40.134+0000", "adminApproved" : "2016-08-18T13:57:04.000+0000", "adminApprover" : { "otype" : "Admin", "mtid" : 10039288, "link" : "/api/admin/10039288", "label" : "Szmolyán Mária (BME 4 admin - INAKTÍV)", "familyName" : "Szmolyán", "givenName" : "Mária", "published" : true, "oldId" : 10039288, "snippet" : true }, "validated" : "2021-05-21T20:38:50.430+0000", "validator" : { "otype" : "Admin", "mtid" : 10015181, "link" : "/api/admin/10015181", "label" : "Nagy Eszter (SZTA admi, admin)", "familyName" : "Nagy", "givenName" : "Eszter", "published" : true, "oldId" : 10015181, "snippet" : true }, "core" : true, "citation" : true, "publicationPending" : false, "type" : { "otype" : "PublicationType", "mtid" : 24, "link" : "/api/publicationtype/24", "label" : "Folyóiratcikk", "code" : 24, "otypeName" : "JournalArticle", "listPosition" : 1, "published" : true, "oldId" : 24, "snippet" : true }, "subType" : { "otype" : "SubType", "mtid" : 10000059, "link" : "/api/subtype/10000059", "label" : "Szakcikk (Folyóiratcikk)", "name" : "Szakcikk", "nameEng" : "Article", "docType" : { "otype" : "PublicationType", "mtid" : 24, "link" : "/api/publicationtype/24", "label" : "Folyóiratcikk", "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" : "Tudományos", "published" : true, "oldId" : 1, "snippet" : true }, "languages" : [ { "otype" : "Language", "mtid" : 10002, "link" : "/api/language/10002", "label" : "Angol", "name" : "Angol", "nameEng" : "English", "published" : true, "oldId" : 2, "snippet" : true } ], "firstAuthor" : "Molnár, Vince", "authorships" : [ { "otype" : "PersonAuthorship", "mtid" : 7671844, "link" : "/api/authorship/7671844", "label" : "Molnár, Vince ✉ [Molnár, Vince (informatika), szerző] Méréstechnika és Információs Rendszerek Tanszék (BME / VIK)", "listPosition" : 1, "share" : 0.2, "first" : true, "last" : false, "corresponding" : true, "author" : { "otype" : "Author", "mtid" : 10049620, "link" : "/api/author/10049620", "label" : "Molnár Vince (informatika)", "familyName" : "Molnár", "givenName" : "Vince", "published" : true, "oldId" : 10049620, "snippet" : true }, "familyName" : "Molnár", "givenName" : "Vince", "authorTyped" : true, "editorTyped" : false, "otherTyped" : false, "type" : { "otype" : "AuthorshipType", "mtid" : 1, "link" : "/api/authorshiptype/1", "label" : "Szerző", "code" : 0, "published" : true, "oldId" : 0, "snippet" : true }, "published" : false, "oldId" : 23849728, "snippet" : true }, { "otype" : "PersonAuthorship", "mtid" : 7671845, "link" : "/api/authorship/7671845", "label" : "Vörös, András [Vörös, András (informatika), szerző] Méréstechnika és Információs Rendszerek Tanszék (BME / VIK)", "listPosition" : 2, "share" : 0.2, "first" : false, "last" : false, "author" : { "otype" : "Author", "mtid" : 10042280, "link" : "/api/author/10042280", "label" : "Vörös András (informatika)", "familyName" : "Vörös", "givenName" : "András", "published" : true, "oldId" : 10042280, "snippet" : true }, "familyName" : "Vörös", "givenName" : "András", "authorTyped" : true, "editorTyped" : false, "otherTyped" : false, "type" : { "otype" : "AuthorshipType", "mtid" : 1, "link" : "/api/authorshiptype/1", "label" : "Szerző", "code" : 0, "published" : true, "oldId" : 0, "snippet" : true }, "published" : false, "oldId" : 23849727, "snippet" : true }, { "otype" : "PersonAuthorship", "mtid" : 7671846, "link" : "/api/authorship/7671846", "label" : "Darvas, Dániel [Darvas, Dániel (Informatika), szerző] Méréstechnika és Információs Rendszerek Tanszék (BME / VIK)", "listPosition" : 3, "share" : 0.2, "first" : false, "last" : false, "author" : { "otype" : "Author", "mtid" : 10046994, "link" : "/api/author/10046994", "label" : "Darvas Dániel (Informatika)", "familyName" : "Darvas", "givenName" : "Dániel", "published" : true, "oldId" : 10046994, "snippet" : true }, "familyName" : "Darvas", "givenName" : "Dániel", "authorTyped" : true, "editorTyped" : false, "otherTyped" : false, "type" : { "otype" : "AuthorshipType", "mtid" : 1, "link" : "/api/authorshiptype/1", "label" : "Szerző", "code" : 0, "published" : true, "oldId" : 0, "snippet" : true }, "published" : false, "oldId" : 23849726, "snippet" : true }, { "otype" : "PersonAuthorship", "mtid" : 7671847, "link" : "/api/authorship/7671847", "label" : "Bartha, Tamás [Bartha, Tamás (Hibatűrő rendszerek), szerző] Rendszer és Irányításelméleti Kutatólaboratórium (HRN SZTAKI)", "listPosition" : 4, "share" : 0.2, "first" : false, "last" : false, "author" : { "otype" : "Author", "mtid" : 10002401, "link" : "/api/author/10002401", "label" : "Bartha Tamás (Hibatűrő rendszerek)", "familyName" : "Bartha", "givenName" : "Tamás", "published" : true, "oldId" : 10002401, "snippet" : true }, "familyName" : "Bartha", "givenName" : "Tamás", "authorTyped" : true, "editorTyped" : false, "otherTyped" : false, "type" : { "otype" : "AuthorshipType", "mtid" : 1, "link" : "/api/authorshiptype/1", "label" : "Szerző", "code" : 0, "published" : true, "oldId" : 0, "snippet" : true }, "published" : false, "oldId" : 23849725, "snippet" : true }, { "otype" : "PersonAuthorship", "mtid" : 7671848, "link" : "/api/authorship/7671848", "label" : "Majzik, István [Majzik, István (Műszaki informatika), szerző] Méréstechnika és Információs Rendszerek Tanszék (BME / VIK)", "listPosition" : 5, "share" : 0.2, "first" : false, "last" : true, "author" : { "otype" : "Author", "mtid" : 10001448, "link" : "/api/author/10001448", "label" : "Majzik István (Műszaki informatika)", "familyName" : "Majzik", "givenName" : "István", "published" : true, "oldId" : 10001448, "snippet" : true }, "familyName" : "Majzik", "givenName" : "István", "authorTyped" : true, "editorTyped" : false, "otherTyped" : false, "type" : { "otype" : "AuthorshipType", "mtid" : 1, "link" : "/api/authorshiptype/1", "label" : "Szerző", "code" : 0, "published" : true, "oldId" : 0, "snippet" : true }, "published" : false, "oldId" : 23849724, "snippet" : true } ], "title" : "Component-wise incremental LTL model checking", "identifiers" : [ { "otype" : "PublicationIdentifier", "mtid" : 1074297, "link" : "/api/publicationidentifier/1074297", "label" : "DOI: 10.1007/s00165-015-0347-x", "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 }, "oaType" : "PAY", "oaFree" : false, "validState" : "IDENTICAL", "idValue" : "10.1007/s00165-015-0347-x", "realUrl" : "https://doi.org/10.1007/s00165-015-0347-x", "published" : false, "oldId" : 1319043, "snippet" : true }, { "otype" : "PublicationIdentifier", "mtid" : 1074300, "link" : "/api/publicationidentifier/1074300", "label" : "SZTAKI: 8941", "source" : { "otype" : "SwordSource", "mtid" : 86, "link" : "/api/publicationsource/86", "label" : "SZTAKI", "type" : { "otype" : "PublicationSourceType", "mtid" : 10007, "link" : "/api/publicationsourcetype/10007", "label" : "Repozitórium", "mayHaveOa" : true, "published" : true, "snippet" : true }, "name" : "SZTAKI", "nameEng" : "SZTAKI", "linkPattern" : "https://eprints.sztaki.hu/@@@", "publiclyVisible" : true, "published" : true, "oldId" : 86, "snippet" : true }, "oaType" : "GREEN", "oaFree" : false, "validState" : "NO", "idValue" : "8941", "realUrl" : "https://eprints.sztaki.hu/8941", "published" : false, "oldId" : 1521797, "snippet" : true }, { "otype" : "PublicationIdentifier", "mtid" : 1074295, "link" : "/api/publicationidentifier/1074295", "label" : "WoS: 000376062700002", "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 }, "oaFree" : false, "validState" : "IDENTICAL", "idValue" : "000376062700002", "realUrl" : "https://www.webofscience.com/wos/woscc/full-record/000376062700002", "published" : false, "oldId" : 1382331, "snippet" : true }, { "otype" : "PublicationIdentifier", "mtid" : 1074296, "link" : "/api/publicationidentifier/1074296", "label" : "Scopus: 84952919510", "source" : { "otype" : "PlainSource", "mtid" : 3, "link" : "/api/publicationsource/3", "label" : "Scopus", "type" : { "otype" : "PublicationSourceType", "mtid" : 10003, "link" : "/api/publicationsourcetype/10003", "label" : "Indexelő adatbázis", "mayHaveOa" : false, "published" : true, "snippet" : true }, "name" : "Scopus", "linkPattern" : "http://www.scopus.com/record/display.url?origin=inward&eid=2-s2.0-@@@", "publiclyVisible" : true, "published" : true, "oldId" : 3, "snippet" : true }, "oaFree" : false, "validState" : "NO", "idValue" : "84952919510", "realUrl" : "http://www.scopus.com/record/display.url?origin=inward&eid=2-s2.0-84952919510", "published" : false, "oldId" : 1319103, "snippet" : true }, { "otype" : "PublicationIdentifier", "mtid" : 1074299, "link" : "/api/publicationidentifier/1074299", "label" : "Teljes dokumentum: http://petridotnet.inf.mit.bme.hu/publications/FAOC2015_MolnarEtAl.pdf", "source" : { "otype" : "PlainSource", "mtid" : 39, "link" : "/api/publicationsource/39", "label" : "Teljes dokumentum", "type" : { "otype" : "PublicationSourceType", "mtid" : 10006, "link" : "/api/publicationsourcetype/10006", "label" : "Link", "mayHaveOa" : true, "published" : true, "snippet" : true }, "name" : "Teljes dokumentum", "nameEng" : "Teljes dokumentum", "linkPattern" : "@@@", "publiclyVisible" : true, "published" : true, "oldId" : 39, "snippet" : true }, "oaType" : "GOLD", "oaFree" : false, "validState" : "NO", "idValue" : "http://petridotnet.inf.mit.bme.hu/publications/FAOC2015_MolnarEtAl.pdf", "realUrl" : "http://petridotnet.inf.mit.bme.hu/publications/FAOC2015_MolnarEtAl.pdf", "published" : false, "oldId" : 1319044, "snippet" : true }, { "otype" : "PublicationIdentifier", "mtid" : 1074298, "link" : "/api/publicationidentifier/1074298", "label" : "Google scholar: 18108012384752200860", "source" : { "otype" : "PlainSource", "mtid" : 12, "link" : "/api/publicationsource/12", "label" : "Google scholar", "type" : { "otype" : "PublicationSourceType", "mtid" : 10003, "link" : "/api/publicationsourcetype/10003", "label" : "Indexelő adatbázis", "mayHaveOa" : false, "published" : true, "snippet" : true }, "name" : "Google scholar", "linkPattern" : "http://scholar.Google.com/scholar?hl=en&lr=&cluster=@@@", "publiclyVisible" : true, "published" : true, "oldId" : 12, "snippet" : true }, "oaFree" : false, "validState" : "NO", "idValue" : "18108012384752200860", "realUrl" : "http://scholar.Google.com/scholar?hl=en&lr=&cluster=18108012384752200860", "published" : false, "oldId" : 1319099, "snippet" : true } ], "journal" : { "otype" : "Journal", "mtid" : 10005652, "link" : "/api/journal/10005652", "label" : "FORMAL ASPECTS OF COMPUTING 0934-5043 1433-299X", "pIssn" : "0934-5043", "eIssn" : "1433-299X", "reviewType" : "REVIEWED", "noIF" : false, "sciIndexed" : true, "scopusIndexed" : true, "hungarian" : false, "published" : true, "oldId" : 10005652, "snippet" : true }, "volume" : "28", "issue" : "3", "firstPage" : "345", "lastPage" : "379", "firstPageOrInternalIdForSort" : "345", "pageLength" : 35, "publishedYear" : 2016, "abstractText" : "Efficient symbolic and explicit-state model checking \napproaches have been developed for the verification of linear \ntime temporal \nlogic (LTL) properties. Several attempts have been made to \ncombine the advantages of the various algorithms. Model \nchecking LTL \nproperties usually poses two challenges: one must compute the \nsynchronous product of the state space and the automaton \nmodel of the \ndesired property, then look for counterexamples that is \nreduced to finding strongly connected components (SCCs) in \nthe state space \nof the product. In case of concurrent systems, where the \nphenomenon of state space explosion often prevents the \nsuccessful \nverification, the so-called saturation algorithm has proved \nits efficiency in state space exploration. This paper \nproposes a new \napproach that leverages the saturation algorithm both as an \niteration strategy constructing the product directly, as well \nas in a \nnew fixed-point computation algorithm to find strongly \nconnected components on-the-fly by incrementally processing \nthe components \nof the model. Complementing the search for SCCs, explicit \ntechniques and component-wise abstractions are used to prove \nthe absence \nof counterexamples. The resulting on-the-fly, incremental LTL \nmodel checking algorithm proved to scale well with the size \nof \nmodels, as the evaluation on models of the Model Checking \nContest suggests.", "subjects" : [ { "otype" : "Classification", "mtid" : 10057, "link" : "/api/classification/10057", "label" : "Elméleti számítástudomány, formális módszerek, kvantumszámítástechnika", "published" : true, "snippet" : true }, { "otype" : "Classification", "mtid" : 10003, "link" : "/api/classification/10003", "label" : "Matematika", "published" : true, "snippet" : true }, { "otype" : "Classification", "mtid" : 10614, "link" : "/api/classification/10614", "label" : "Matematikai modellezés", "published" : true, "snippet" : true }, { "otype" : "Classification", "mtid" : 11742, "link" : "/api/classification/11742", "label" : "Modell alapú szoftverfejlesztés", "published" : true, "snippet" : true }, { "otype" : "Classification", "mtid" : 10034, "link" : "/api/classification/10034", "label" : "Számítás- és információtudomány", "published" : true, "snippet" : true } ], "digital" : null, "printed" : null, "sourceYear" : 2016, "foreignEdition" : true, "foreignLanguage" : true, "fullPublication" : true, "conferencePublication" : false, "nationalOrigin" : true, "missingAuthor" : false, "oaType" : "GOLD", "oaCheckDate" : "2024-02-18", "oaFree" : true, "oaLink" : "http://petridotnet.inf.mit.bme.hu/publications/FAOC2015_MolnarEtAl.pdf", "oaByAuthor" : { "otype" : "Admin", "mtid" : 10015181, "link" : "/api/admin/10015181", "label" : "Nagy Eszter (SZTA admi, admin)", "familyName" : "Nagy", "givenName" : "Eszter", "published" : true, "oldId" : 10015181, "snippet" : true }, "citationCount" : 8, "citationCountUnpublished" : 0, "citationCountWoOther" : 7, "independentCitCountWoOther" : 3, "nationalOriginCitationCount" : 6, "foreignEditionCitationCount" : 5, "doiCitationCount" : 6, "wosCitationCount" : 4, "scopusCitationCount" : 6, "wosScopusCitationCount" : 6, "wosScopusCitationCountWoOther" : 6, "wosScopusIndependentCitationCount" : 3, "wosScopusIndependentCitationCountWoOther" : 3, "independentCitationCount" : 4, "selfCitationCount" : 4, "unhandledCitationCount" : 0, "citingPubCount" : 8, "independentCitingPubCount" : 4, "citingPubCountWoOther" : 7, "independentCitingPubCountWoOther" : 3, "unhandledCitingPubCount" : 0, "citedPubCount" : 1, "citedCount" : 1, "pubStats" : { "types" : [ { "type" : "Folyóiratcikk", "typeEng" : "Journal Article", "code" : 24, "count" : 4 }, { "type" : "Könyvrészlet", "typeEng" : "Chapter in Book", "code" : 25, "count" : 3 }, { "type" : "Könyv", "typeEng" : "Book", "code" : 23, "count" : 0 }, { "type" : "Egyéb konferenciaközlemény", "typeEng" : "Conference paper", "code" : 31, "count" : 0 }, { "type" : "Egyéb konferenciakötet", "typeEng" : "Conference proceedings", "code" : 32, "count" : 0 }, { "type" : "Oltalmi formák", "typeEng" : "Protection forms", "code" : 26, "count" : 0 }, { "type" : "Disszertáció", "typeEng" : "Thesis", "code" : 28, "count" : 1 }, { "type" : "Egyéb", "typeEng" : "Miscellaneous", "code" : 29, "count" : 0 }, { "type" : "Alkotás", "typeEng" : "Achievement", "code" : 22, "count" : 0 }, { "type" : "Kutatási adat", "typeEng" : "Research data", "code" : 33, "count" : 0 } ], "citationTypes" : [ { "type" : "Folyóiratcikk", "typeEng" : "Journal Article", "code" : 24, "countUnknown" : 0, "countIndependent" : 0, "countSelfCitation" : 0 }, { "type" : "Könyvrészlet", "typeEng" : "Chapter in Book", "code" : 25, "countUnknown" : 0, "countIndependent" : 0, "countSelfCitation" : 0 }, { "type" : "Könyv", "typeEng" : "Book", "code" : 23, "countUnknown" : 0, "countIndependent" : 0, "countSelfCitation" : 0 }, { "type" : "Egyéb konferenciaközlemény", "typeEng" : "Conference paper", "code" : 31, "countUnknown" : 0, "countIndependent" : 0, "countSelfCitation" : 0 }, { "type" : "Egyéb konferenciakötet", "typeEng" : "Conference proceedings", "code" : 32, "countUnknown" : 0, "countIndependent" : 0, "countSelfCitation" : 0 }, { "type" : "Oltalmi formák", "typeEng" : "Protection forms", "code" : 26, "countUnknown" : 0, "countIndependent" : 0, "countSelfCitation" : 0 }, { "type" : "Disszertáció", "typeEng" : "Thesis", "code" : 28, "countUnknown" : 0, "countIndependent" : 0, "countSelfCitation" : 0 }, { "type" : "Egyéb", "typeEng" : "Miscellaneous", "code" : 29, "countUnknown" : 0, "countIndependent" : 0, "countSelfCitation" : 0 }, { "type" : "Alkotás", "typeEng" : "Achievement", "code" : 22, "countUnknown" : 0, "countIndependent" : 0, "countSelfCitation" : 0 }, { "type" : "Kutatási adat", "typeEng" : "Research data", "code" : 33, "countUnknown" : 0, "countIndependent" : 0, "countSelfCitation" : 0 } ], "years" : [ { "year" : 2016, "publicationCount" : 0, "citationCount" : 3, "independentCitationCount" : 2, "citingPubCount" : 3, "independentCitingPubCount" : 2, "oaStats" : null, "oaStats2" : null }, { "year" : 2017, "publicationCount" : 0, "citationCount" : 3, "independentCitationCount" : 2, "citingPubCount" : 3, "independentCitingPubCount" : 2, "oaStats" : null, "oaStats2" : null }, { "year" : 2018, "publicationCount" : 0, "citationCount" : 1, "independentCitationCount" : 0, "citingPubCount" : 1, "independentCitingPubCount" : 0, "oaStats" : null, "oaStats2" : null }, { "year" : 2019, "publicationCount" : 0, "citationCount" : 1, "independentCitationCount" : 0, "citingPubCount" : 1, "independentCitingPubCount" : 0, "oaStats" : null, "oaStats2" : null } ] }, "ratings" : [ { "otype" : "SjrRating", "mtid" : 10963706, "link" : "/api/sjrrating/10963706", "label" : "sjr:Q2 (2016) Scopus - Software FORMAL ASPECTS OF COMPUTING 0934-5043", "listPos" : 151, "rankValue" : 0.49, "type" : "journal", "ratingType" : { "otype" : "RatingType", "mtid" : 10002, "link" : "/api/ratingtype/10002", "label" : "sjr", "code" : "sjr", "published" : true, "snippet" : true }, "subject" : { "otype" : "ClassificationExternal", "mtid" : 1712, "link" : "/api/classificationexternal/1712", "label" : "Scopus - Software", "published" : true, "oldId" : 1712, "snippet" : true }, "ranking" : "Q2", "calculation" : "DIRECT", "published" : true, "snippet" : true } ], "ratingsForSort" : "Q2", "hasCitationDuplums" : false, "inSelectedPubs" : "10049620,10042280", "userChangeableUntil" : "2016-08-18T13:57:04.000+0000", "publishDate" : "2016-02-26T13:38:10.000+0000", "directInstitutesForSort" : "Méréstechnika és Információs Rendszerek Tanszék (BME / VIK); Rendszer és Irányításelméleti Kutatólaboratórium (HRN SZTAKI)", "ownerAuthorCount" : 5, "ownerInstituteCount" : 16, "directInstituteCount" : 2, "authorCount" : 5, "contributorCount" : 0, "hasQualityFactor" : true, "link" : "/api/publication/3025948", "label" : "Molnár Vince et al. Component-wise incremental LTL model checking. (2016) FORMAL ASPECTS OF COMPUTING 0934-5043 1433-299X 28 3 345-379", "template" : "