Zobrazeno 1 - 10
of 19
pro vyhledávání: '"Naiyong Jin"'
Publikováno v:
STTT
STTT, 2013, 15 (5-6), pp.541-561. ⟨10.1007/s10009-012-0222-5⟩
International Journal on Software Tools for Technology Transfer
STTT, 2013, 15 (5-6), pp.541-561. ⟨10.1007/s10009-012-0222-5⟩
International Journal on Software Tools for Technology Transfer
In this paper, we show how to exploit the structure of some automata-based construction to efficiently solve the LTL synthesis problem. We focus on a construction proposed in Schewe and Finkbeiner that reduces the synthesis problem to a safety game,
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::94ae165995b06bafb925dacc4ba514d0
https://doi.org/10.1007/s10009-012-0222-5
https://doi.org/10.1007/s10009-012-0222-5
Publikováno v:
Computer Aided Verification ISBN: 9783642397981
CAV
CAV
SystemVerilog Assertions SVA, as well as Property Specification Language PSL are linear temporal logics based on LTL [14], extended with regular expressions and local variables. In [6] Bustan and Havlicek show that the local variable extensions, as w
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::28a9d02c95af96686a7ddcb2ac5050f8
https://doi.org/10.1007/978-3-642-39799-8_13
https://doi.org/10.1007/978-3-642-39799-8_13
Publikováno v:
Computer Aided Verification (CAV)
Computer Aided Verification (CAV), 2012, Unknown, Unknown Region. pp.652-657, ⟨10.1007/978-3-642-31424-7_45⟩
Lecture Notes in Computer Science
Computer Aided Verification ISBN: 9783642314230
CAV
Computer Aided Verification (CAV), 2012, Unknown, Unknown Region. pp.652-657, ⟨10.1007/978-3-642-31424-7_45⟩
Lecture Notes in Computer Science
Computer Aided Verification ISBN: 9783642314230
CAV
We present Acacia+, a tool for solving the LTL realizability and synthesis problems. We use recent approaches that reduce these problems to safety games, and can be solved efficiently by symbolic incremental algorithms based on antichains. The reduct
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::169c52cd0d18c7b54b3134bd6edef2eb
https://hal.archives-ouvertes.fr/hal-01196263
https://hal.archives-ouvertes.fr/hal-01196263
Publikováno v:
Formal Methods in System Design
Formal Methods in System Design, Springer Verlag, 2011, 39 (3), pp.261-296
Formal Methods in System Design, Springer Verlag, 2011, 39 (3), pp.261-296
In this paper, we present new monolithic and compositional algorithms to solve the LTL realizability problem. Those new algorithms are based on a reduction of the LTL realizability problem to a game whose winning condition is defined by a universal a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ac74af1ed6aa7b86a6f2c278078f8189
https://hal.archives-ouvertes.fr/hal-01196265
https://hal.archives-ouvertes.fr/hal-01196265
Publikováno v:
8th International Symposium on Automated Technology for Verification and Analysis (ATVA)
8th International Symposium on Automated Technology for Verification and Analysis (ATVA), Sep 2010, Singapore, Singapore
Automated Technology for Verification and Analysis ISBN: 9783642156427
ATVA
8th International Symposium on Automated Technology for Verification and Analysis (ATVA), Sep 2010, Singapore, Singapore
Automated Technology for Verification and Analysis ISBN: 9783642156427
ATVA
International audience; In this paper, we provide two compositional algorithms to solve safety games and apply them to provide compositional algorithms for the LTL synthesis problem. We have implemented those new compositional algorithms, and we demo
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e261700e3e80d19267ab04ff4823cd43
https://hal.inria.fr/inria-00509966
https://hal.inria.fr/inria-00509966
Publikováno v:
Unifying Theories of Programming ISBN: 9783642145209
UTP
UTP
As a system-level modelling language, SystemC possesses several novel features such as delayed notifications, notification cancelling, notification overriding and delta-cycle. It is challenging to formalise SystemC. In this paper, we study the denota
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5b81f666e6f3346dd2cc1216745dcd6c
https://doi.org/10.1007/978-3-642-14521-6_15
https://doi.org/10.1007/978-3-642-14521-6_15
Publikováno v:
Computer Aided Verification
Computer Aided Verification, Jun 2009, Grenoble, France. pp.263-277, ⟨10.1007/978-3-642-02658-4_22⟩
Computer Aided Verification ISBN: 9783642026577
CAV
Computer Aided Verification, Jun 2009, Grenoble, France. pp.263-277, ⟨10.1007/978-3-642-02658-4_22⟩
Computer Aided Verification ISBN: 9783642026577
CAV
International audience; In this paper, we study the structure of underlying automata based constructions for solving the LTL realizability and synthesis problem. We show how to reduce the LTL realizability problem to a game with an observer that chec
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::bf504fd68f471e76e3b621715d663e5f
https://hal.inria.fr/inria-00489952/document
https://hal.inria.fr/inria-00489952/document
Publikováno v:
FSKD (2)
Model checking of 3-valued logical formulae is analyzed. The solution is presented when the value of model checking for a 3-valued logical formula is UNKNOWN. In this paper, a proof system is established on a 3-valued logic, with additional proof ste
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::3d1dffd8094eb4fc9c6e669d1eec2991
https://doi.org/10.1109/fskd.2008.589
https://doi.org/10.1109/fskd.2008.589
Publikováno v:
ICECCS
In PSL, behavioral properties of an IP core and its environment are directed by different directives. Improperly directed properties will severely impact the validity of refinement verification, specification assurance, and the evolution of specifica
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::803c4702a8928337abc6b5cf5d2e8862
https://doi.org/10.1109/iceccs.2008.13
https://doi.org/10.1109/iceccs.2008.13
Autor:
Huibiao Zhu, Naiyong Jin
Publikováno v:
Communications in Computer and Information Science ISBN: 9783540884781
ISoLA
ISoLA
One purpose of Property Assurance is to check the satisfiability of properties. The Sequential Extended Regular Expressions (SEREs) play important roles in composing PSL properties. The SEREs are regular expressions with repetition and conjunction. C
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::82491a776daaee12e468276a47f518dd
https://doi.org/10.1007/978-3-540-88479-8_17
https://doi.org/10.1007/978-3-540-88479-8_17