全文获取类型
收费全文 | 67篇 |
免费 | 3篇 |
专业分类
电工技术 | 1篇 |
化学工业 | 9篇 |
建筑科学 | 2篇 |
轻工业 | 1篇 |
无线电 | 3篇 |
一般工业技术 | 3篇 |
冶金工业 | 8篇 |
自动化技术 | 43篇 |
出版年
2023年 | 1篇 |
2022年 | 2篇 |
2021年 | 1篇 |
2018年 | 2篇 |
2017年 | 1篇 |
2016年 | 3篇 |
2014年 | 2篇 |
2013年 | 2篇 |
2012年 | 2篇 |
2011年 | 1篇 |
2010年 | 5篇 |
2009年 | 4篇 |
2008年 | 2篇 |
2007年 | 2篇 |
2006年 | 3篇 |
2005年 | 6篇 |
2004年 | 4篇 |
2003年 | 5篇 |
2002年 | 4篇 |
2001年 | 5篇 |
2000年 | 1篇 |
1997年 | 2篇 |
1995年 | 2篇 |
1993年 | 3篇 |
1988年 | 1篇 |
1986年 | 1篇 |
1984年 | 1篇 |
1978年 | 1篇 |
1969年 | 1篇 |
排序方式: 共有70条查询结果,搜索用时 0 毫秒
1.
Orna Kupferman Giuseppe Perelli Moshe Y. Vardi 《Annals of Mathematics and Artificial Intelligence》2016,78(1):3-20
Synthesis is the automated construction of a system from its specification. The system has to satisfy its specification in all possible environments. The environment often consists of agents that have objectives of their own. Thus, it makes sense to soften the universal quantification on the behavior of the environment and take the objectives of its underlying agents into an account. Fisman et al. introduced rational synthesis: the problem of synthesis in the context of rational agents. The input to the problem consists of temporal logic formulas specifying the objectives of the system and the agents that constitute the environment, and a solution concept (e.g., Nash equilibrium). The output is a profile of strategies, for the system and the agents, such that the objective of the system is satisfied in the computation that is the outcome of the strategies, and the profile is stable according to the solution concept; that is, the agents that constitute the environment have no incentive to deviate from the strategies suggested to them. In this paper we continue to study rational synthesis. First, we suggest an alternative definition to rational synthesis, in which the agents are rational but not cooperative. We call such problem strong rational synthesis. In the strong rational synthesis setting, one cannot assume that the agents that constitute the environment take into account the strategies suggested to them. Accordingly, the output is a strategy for the system only, and the objective of the system has to be satisfied in all the compositions that are the outcome of a stable profile in which the system follows this strategy. We show that strong rational synthesis is 2ExpTime-complete, thus it is not more complex than traditional synthesis or rational synthesis. Second, we study a richer specification formalism, where the objectives of the system and the agents are not Boolean but quantitative. In this setting, the objective of the system and the agents is to maximize their outcome. The quantitative setting significantly extends the scope of rational synthesis, making the game-theoretic approach much more relevant. Finally, we enrich the setting to one that allows coalitions of agents that constitute the system or the environment. 相似文献
2.
Orna Grumberg Moshe Y. Vardi Joseph Sifakis Rajeev Alur 《Formal Methods in System Design》2012,40(2):117-120
The 2010 CAV (Computer-Aided Verification) award was awarded to Kenneth L. McMillan of Cadence Research Laboratories for a
series of fundamental contributions resulting in significant advances in scalability of model checking tools. The annual award
recognizes a specific fundamental contribution or a series of outstanding contributions to the CAV field. 相似文献
3.
Vilchinsky Noa; Dekel Rachel; Leibowitz Morton; Reges Orna; Khaskia Abid; Mosseri Morris 《Canadian Metallurgical Quarterly》2011,30(4):411
Objective: The current prospective study explored how male cardiac patients' perceptions of received support (i.e., active engagement, protective buffering, and overprotection) moderated the associations between female partners' perceptions of provided support and patients' recovery outcomes: psychological well-being, cholesterol levels, and smoking cessation. Methods: Couples (N = 86) completed surveys at the initial hospitalization after patients' Acute Coronary Syndrome (ACS), and 1 and 6 months later. Partners' ways of providing support and patients' concurrent perceptions of these ways were measured using the Ways of Giving Support Questionnaire; patients' depressive and anxiety symptoms were measured using the Brief Symptom Inventory (BSI). Patients' cholesterol levels were assessed during hospitalization and 6 months later, and smoking habits were reported by the patients. Results: Female partners' protective buffering was positively associated with male patients' depressive symptoms at follow-up only when male patients' own perceptions of partners' protective buffering were low. Female partners' active engagement was positively associated with better odds for male patients' cessation of smoking only when patients' own perceptions of partners' active engagement were high. Finally, female partners' overprotection was associated with higher levels of male patients' harmful blood lipids at follow-up, but only when patients' own perceptions of partners' overprotection were high. Conclusions: As hypothesized, the effect of partners' perceptions of support provided on patients' recovery was moderated by patients' own perceptions of the support received. The effect of this interaction was determined by the specific types of support provided or received and by the specific recovery outcome that was measured. The clinical and theoretical implications of the findings are discussed. (PsycINFO Database Record (c) 2011 APA, all rights reserved) 相似文献
4.
Luboš Brim Orna Grumberg 《International Journal on Software Tools for Technology Transfer (STTT)》2005,7(1):1-3
This special section is devoted to a selection of contributions originally presented at the 1st International Workshop on Parallel and Distributed Model Checking (PDMC 2002), which took place in Brno, Czech Republic in September 2002 as a satellite event of the 13th conference on concurrency theory (CONCUR 2002). The growing importance of automated formal verification in industry is driving a growing interest in those aspects that have a direct impact on its applicability to real-world problems. One of the main technical challenges is in devising tools that allow one to handle large state spaces. In the last several years numerous approaches to solving this problem have been developed. Recently there has been increasing interest in parallelizing and distributing verification techniques. Papers that appear in this special section provide an interesting sampling of typical approaches in this direction. 相似文献
5.
In implementation verification, we check that an implementation is correct with respect to a specification by checking whether the behaviors of a transition system that models the program's implementation correlate with the behaviors of a transition system that models its specification. In this paper, we investigate the effect of concurrency on the complexity of implementation verification. We consider trace-based and tree-based approaches to the verification of concurrent transition systems, with and without fairness. Our results show that in almost all cases the complexity of the problem is exponentially harder than that of the sequential case. Thus, as in the model-checking verification methodology, the state-explosion problem cannot be avoided. 相似文献
6.
Sérgio?CamposEmail author Orna?Grumberg Karen?Yorav Copty?Fady 《International Journal on Software Tools for Technology Transfer (STTT)》2004,6(2):174-182
The task of finding a set of test sequences that provides good coverage of industrial circuits is infeasible because of the size of the circuits. For small critical subcircuits of the design, however, designers can create a set of test sequences that achieve good coverage. These sequences cannot be used on the full design because the inputs to the subcircuit may not be accessible. In this work we present an efficient test generation algorithm that receives a test sequence created for the subcircuit and finds a test sequence for the full design that reproduces the given sequence on the subcircuit. The algorithm uses a new technique called dynamic transition relations to increase its efficiency .The most common and most expensive step in our algorithm is the computation of the set of predecessors of a set of states. To make this computation more efficient we exploit a partitioning of the transition relation into a set of simpler relations. At every step we use only those that are necessary, resulting in a smaller relation than the original one. A different relation is used for each step, hence the name dynamic transition relations. The same idea can be used to improve symbolic model checking for the temporal logic CTL.We have implemented the new method in SMV and run it on several large circuits. Our experiments indicate that the new method can provide gains of up to two orders of magnitude in time and space during verification. These results show that dynamic transition relations can make it possible to verify circuits that were previously unmanageable due to their size and complexity . 相似文献
7.
Symbolic model checking, which enables the automatic verification of large systems, proceeds by calculating expressions that represent state sets. Traditionally, symbolic model-checking tools are based on backward state traversal; their basic operation is the function pre, which, given a set of states, returns the set of all predecessor states. This is because specifiers usually employ formalisms with future-time modalities, which are naturally evaluated by iterating applications of pre. It has been shown experimentally that symbolic model checking can perform significantly better if it is based, instead, on forward state traversal; in this case, the basic operation is the function post, which, given a set of states, returns the set of all successor states. This is because forward state traversal can ensure that only parts of the state space that are reachable from an initial state and relevant for the satisfaction or violation of the specification are explored; that is, errors can be detected as soon as possible.In this paper, we investigate which specifications can be checked by symbolic forward state traversal. We formulate the problems of symbolic backward and forward model checking by means of two -calculi. The pre- calculus is based on the pre operation, and the post- calculus is based on the post operation. These two -calculi induce query logics, which augment fixpoint expressions with a boolean emptiness query. Using query logics, we are able to relate and compare the symbolic backward and forward approaches. In particular, we prove that all -regular (linear-time) specifications can be expressed as post- queries, and therefore checked using symbolic forward state traversal. On the other hand, we show that there are simple branching-time specifications that cannot be checked in this way. 相似文献
8.
Alessandro Cimatti Orna Grumberg 《Electronic Notes in Theoretical Computer Science》2001,23(2):127-128
This volume contains the proceedings of the First International Workshop on Symbolic Model Checking (SMC'99), held in Trento, Italy, on July 6, 1999, as part of the Second Federated Logic Conference (FLoC'99).Symbolic model checking is a formal technique for the verification of finite-state concurrent systems. Symbolic model checkers (e.g. SMV, VIS) have been used to verify industrial systems, ranging from hardware to communication protocols to safety critical plants and procedures. Symbolic model checking is the core technique for several industrial verification tools, and is applied in technology transfer projects. The aim of the SMC'99 workshop is to bring together active developers and users of symbolic model checkers, compare state of the art model checking techniques (e.g. compositional reasoning, abstraction, partitioning), discuss experimental results and experience reports, and promising directions for future research.Nine contributions (out of twenty-two submissions) were selected for presentation by the program committee. The workshop program is completed by two keynote invited lectures, given by Ken McMillan (Cadence Labs, USA) on Compositional Reasoning and Abstraction, and Fabio Somenzi (University of Colorado, USA) on Symbolic State ExplorationThanks are due to a number of people who helped to organize and plan the workshop. Among this group are the Program Committee members:
The following people helped in the evaluation of the submissions: Yael Abarbanel-Vinov, Neta Aizenbud-Reshef, Shoham Ben-David, Doron Bustan, Jorge Cuellar, David Deharbe, Cindy Eisner, Ranan Fraer, Edelweis Garcez, Leonid Gluhovsky, Marcelo Glusman, Jae-Young Jang, Shmuel Katz, Sharon Keidar, Monika Maidl, Robi Malik, Anamaria Martins Moreira, Shiri Moran, Peter Päppinghaus, Marco Roveri, Peter Warkentin, Karen Yorav, Jun Yuan, Yunshan Zhu.We would like to thank IBM Haifa Research Laboratory for the financial support to SMC'99. Carola Dori, Morena Carli, Marco Roveri and Adolfo Villafiorita helped in several matters related to the local organization. Finally, we are grateful to Michael Mislove for his constat support during the preparation of this electronic volume.Alessandro Cimatti and Orna Grumberg, Guest Editors 相似文献
Adnan Aziz | (University of Texas at Austin, USA) |
Armin Biere | (Verysys) |
Sergio Campos | (Federal University of Minas Gerais, Brazil) |
Alessandro Cimatti | (IRST, Italy) |
Edmund Clarke | (Carnegie Mellon University, USA) |
Danny Geist | (IBM Haifa, Israel) |
Fausto Giunchiglia | (IRST, Italy) |
Orna Grumberg | (Technion, Israel) |
Markus Kaltenbach | (Siemens, Germany) |
Carl Pixley | (Motorola, USA) |
Full-size table
9.
10.
Tamir Heyman Danny Geist Orna Grumberg Assaf Schuster 《Formal Methods in System Design》2002,21(3):317-338
This paper presents a scalable method for parallelizing symbolic reachability analysis on a distributed-memory environment of workstations. We have developed an adaptive partitioning algorithm that significantly reduces space requirements. The memory balance is maintained by dynamically repartitioning the state space throughout the computation. A compact BDD representation allows coordination by shipping BDDs from one machine to another. This representation allows for different variable orders in the sending and receiving processes. The algorithm uses a distributed termination protocol, with none of the memory modules preserving a complete image of the set of reachable states. No external storage is used on the disk. Rather, we make use of the network, which is much faster.We implemented our method on a standard, loosely-connected environment of workstations, using a high-performance model checker. Initial performance evaluation of several large circuits shows that our method can handle models too large to fit in the memory of a single node. The partitioning algorithm achieves reduction in space, which is linear in the number of workstations employed. A corresponding decrease in space requirements is measured throughout the reachability analysis. Our results show that the relatively slow network does not become a bottleneck, and that computation time is kept reasonably small. 相似文献